From 2d500fe42404f9a451051bd7fefef6b3e50db0a7 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 15 Nov 2012 13:33:13 -0800 Subject: [PATCH] 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. --- model.cc | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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) -- 2.34.1