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 98d7e093add60f8dfde8ad249506a81aabec47d8..a2a0a6d4d39f5c2eaf99caa7e9b743e0acda4ffb 100644 (file)
--- 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)