datarace: make globals static

[model-checker.git] / datarace.cc

diff --git a/datarace.cc b/datarace.cc
index 1ec43be4e8cb72dc246782635fd6497ac8e6ffb3..5f007f36522754960db4c4588c80ee75c2a49ad5 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -8,10 +8,10 @@
 #include "config.h"
 #include "action.h"
 
-struct ShadowTable *root;
-std::vector<struct DataRace *> unrealizedraces;
-void *memory_base;
-void *memory_top;
+static struct ShadowTable *root;
+SnapVector<struct DataRace *> unrealizedraces;
+static void *memory_base;
+static void *memory_top;
 
 
 /** This function initialized the data race detector. */
@@ -150,16 +150,18 @@ bool checkDataRaces()
  */
 void assert_race(struct DataRace *race)
 {
-       char buf[200];
-       char *ptr = buf;
-       ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
-       ptr += sprintf(ptr, "    Access 1: %5s in thread %2d @ clock %3u\n",
+       model->assert_bug(
+                       "Data race detected @ address %p:\n"
+                       "    Access 1: %5s in thread %2d @ clock %3u\n"
+                       "    Access 2: %5s in thread %2d @ clock %3u",
+                       race->address,
                        race->isoldwrite ? "write" : "read",
-                       id_to_int(race->oldthread), race->oldclock);
-       ptr += sprintf(ptr, "    Access 2: %5s in thread %2d @ clock %3u",
+                       id_to_int(race->oldthread),
+                       race->oldclock,
                        race->isnewwrite ? "write" : "read",
-                       id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
-       model->assert_bug(buf);
+                       id_to_int(race->newaction->get_tid()),
+                       race->newaction->get_seq_number()
+               );
 }
 
 /** This function does race detection for a write on an expanded record. */