From: Brian Norris <banorris@uci.edu>
Date: Fri, 16 Nov 2012 22:44:32 +0000 (-0800)
Subject: dataraces: don't print an uninformative "Data race" bug msg
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ecf16617a0c289981925fcd2437595f3a2fce8fe;p=c11tester.git

dataraces: don't print an uninformative "Data race" bug msg

Now that checkDataRaces() handles all bug reporting and assertions on
its own, we don't need an additional bug report message printed by the
caller. In some cases, this means the caller doesn't have any action to
take. In one case (a race immediately-realized from a user thread), we
still need to "bail out" to the model-checker.
---

diff --git a/datarace.cc b/datarace.cc
index 8d913c70..bdfade35 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -103,7 +103,7 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 
 	/* If the race is realized, bail out now. */
 	if (checkDataRaces())
-		model->assert_bug("Data race", true);
+		model->switch_to_master(NULL);
 }
 
 /**
diff --git a/model.cc b/model.cc
index ab16bf82..33e88050 100644
--- a/model.cc
+++ b/model.cc
@@ -446,8 +446,8 @@ bool ModelChecker::next_execution()
 		if (is_deadlocked())
 			assert_bug("Deadlock detected");
 
-		print_bugs();
 		checkDataRaces();
+		print_bugs();
 		printf("\n");
 		print_stats();
 		print_summary();
@@ -917,8 +917,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 	}
 
 	/* See if we have realized a data race */
-	if (checkDataRaces())
-		assert_bug("Data race");
+	checkDataRaces();
 }
 
 /**
@@ -1849,8 +1848,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 	}
 
 	// If we resolved promises or data races, see if we have realized a data race.
-	if (checkDataRaces())
-		assert_bug("Data race");
+	checkDataRaces();
 
 	return updated;
 }