race->isnewwrite=isnewwrite;
race->address=address;
unrealizedraces.push_back(race);
- checkDataRaces();
+
+ /* If the race is realized, bail out now. */
+ if (checkDataRaces()) {
+ model->assert_thread();
+ }
}
/** This function goes through the list of unrealized data races,
* removes the impossible ones, and print the realized ones. */
-void checkDataRaces() {
- if (true) {
+bool checkDataRaces() {
+ if (model->isfeasibleprefix()) {
/* Prune the non-racing unrealized dataraces */
unsigned int i,newloc=0;
for(i=0;i<unrealizedraces.size();i++) {
}
if (newloc!=i)
unrealizedraces.resize(newloc);
- for(i=0;i<unrealizedraces.size();i++) {
- struct DataRace * race=unrealizedraces[i];
- printRace(race);
+
+ 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) {