X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=16d5db4ab280262d1c4439de6544a413f8ba794e;hb=b44d6b0535ac6b10bebd68aca5a69e424a027e38;hp=d9caf9a91e72ef727835a24433ba3496c74f7cd6;hpb=a4d3f2ae3f3a9e2a30cc36c92cee9f83bb09e9b1;p=model-checker.git

diff --git a/model.cc b/model.cc
index d9caf9a..16d5db4 100644
--- a/model.cc
+++ b/model.cc
@@ -197,15 +197,13 @@ void ModelChecker::assert_user_bug(const char *msg)
 /** @brief Print bug report listing for this execution (if any bugs exist) */
 void ModelChecker::print_bugs() const
 {
-	if (execution->have_bug_reports()) {
-		SnapVector<bug_message *> *bugs = execution->get_bugs();
-
-		model_print("Bug report: %zu bug%s detected\n",
-				bugs->size(),
-				bugs->size() > 1 ? "s" : "");
-		for (unsigned int i = 0; i < bugs->size(); i++)
-			(*bugs)[i]->print();
-	}
+	SnapVector<bug_message *> *bugs = execution->get_bugs();
+
+	model_print("Bug report: %zu bug%s detected\n",
+			bugs->size(),
+			bugs->size() > 1 ? "s" : "");
+	for (unsigned int i = 0; i < bugs->size(); i++)
+		(*bugs)[i]->print();
 }
 
 /**
@@ -252,10 +250,12 @@ void ModelChecker::print_stats() const
  */
 void ModelChecker::print_execution(bool printbugs) const
 {
+	model_print("Program output from execution %d:\n",
+			get_execution_number());
 	print_program_output();
 
-	if (params.verbose) {
-		model_print("Earliest divergence point since last feasible execution:\n");
+	if (params.verbose >= 2) {
+		model_print("\nEarliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
 		else
@@ -266,8 +266,10 @@ void ModelChecker::print_execution(bool printbugs) const
 	}
 
 	/* Don't print invalid bugs */
-	if (printbugs)
+	if (printbugs && execution->have_bug_reports()) {
+		model_print("\n");
 		print_bugs();
+	}
 
 	model_print("\n");
 	execution->print_summary();
@@ -483,4 +485,8 @@ void ModelChecker::run()
 
 	model_print("******* Model-checking complete: *******\n");
 	print_stats();
+
+	/* Have the trace analyses dump their output. */
+	for (unsigned int i = 0; i < trace_analyses.size(); i++)
+		trace_analyses[i]->finish();
 }