From: Brian Norris <banorris@uci.edu>
Date: Thu, 15 Nov 2012 21:33:13 +0000 (-0800)
Subject: model: print bug reports at end of each execution
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=2d500fe42404f9a451051bd7fefef6b3e50db0a7;p=c11tester.git

model: print bug reports at end of each execution

This ensures:
- that bug reports are printed only at the end of feasible executions
- that execution summaries are printed only for complete (or halted and
  buggy) executions that are feasible
- that all bug reports will have the same formatting (at least, ones
  that use the 'assert_bug()' function)

Note that deadlocks are the only bugs reported this way right now. I'll
fix that up soon.
---

diff --git a/model.cc b/model.cc
index 98d7e093..a2a0a6d4 100644
--- a/model.cc
+++ b/model.cc
@@ -406,9 +406,7 @@ bool ModelChecker::next_execution()
 
 	num_executions++;
 
-	if (is_deadlocked())
-		printf("ERROR: DEADLOCK\n");
-	if (isfinalfeasible()) {
+	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
@@ -417,12 +415,15 @@ bool ModelChecker::next_execution()
 
 		earliest_diverge = NULL;
 		num_feasible_executions++;
-	}
 
+		if (is_deadlocked())
+			assert_bug("Deadlock detected", false);
 
-	if (isfinalfeasible() || DBG_ENABLED()) {
+		print_bugs();
 		checkDataRaces();
 		print_summary();
+	} else if (DBG_ENABLED()) {
+		print_summary();
 	}
 
 	if ((diverge = get_next_backtrack()) == NULL)