+/** This function goes through the list of unrealized data races,
+ * removes the impossible ones, and print the realized ones. */
+
+bool checkDataRaces() {
+ if (model->isfeasibleprefix()) {
+ /* Prune the non-racing unrealized dataraces */
+ unsigned int i,newloc=0;
+ for(i=0;i<unrealizedraces.size();i++) {
+ struct DataRace * race=unrealizedraces[i];
+ if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
+ unrealizedraces[newloc++]=race;
+ }
+ }
+ if (newloc!=i)
+ unrealizedraces.resize(newloc);
+
+ if (unrealizedraces.size()!=0) {
+ /* We have an actual realized race. */
+ for(i=0;i<unrealizedraces.size();i++) {
+ struct DataRace * race=unrealizedraces[i];
+ printRace(race);
+ }
+ return true;
+ }
+ }
+ return false;
+}
+
+void printRace(struct DataRace *race)
+{
+ printf("Datarace detected @ address %p:\n", race->address);
+ printf(" Access 1: %5s in thread %2d @ clock %3u\n",
+ race->isoldwrite ? "write" : "read",
+ id_to_int(race->oldthread), race->oldclock);
+ printf(" Access 2: %5s in thread %2d @ clock %3u\n",
+ race->isnewwrite ? "write" : "read",
+ id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
+}
+
+/** This function does race detection for a write on an expanded record. */
+void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {