From f559a99c8394cdd45b493ed546e8a719b9a0dbf5 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 16 Nov 2012 23:55:12 -0800
Subject: [PATCH 1/1] model: refactor end-of-execution output

---
 model.cc | 69 ++++++++++++++++++++++++++++++++------------------------
 model.h  |  1 +
 2 files changed, 41 insertions(+), 29 deletions(-)

diff --git a/model.cc b/model.cc
index 691cd72b..eb5cd347 100644
--- a/model.cc
+++ b/model.cc
@@ -413,6 +413,33 @@ void ModelChecker::print_stats() const
 	model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
 }
 
+/**
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
+ */
+void ModelChecker::print_execution(bool printbugs) const
+{
+	print_program_output();
+
+	if (DBG_ENABLED() || params.verbose) {
+		model_print("Earliest divergence point since last feasible execution:\n");
+		if (earliest_diverge)
+			earliest_diverge->print();
+		else
+			model_print("(Not set)\n");
+
+		model_print("\n");
+		print_stats();
+	}
+
+	/* Don't print invalid bugs */
+	if (printbugs)
+		print_bugs();
+
+	model_print("\n");
+	print_summary();
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -423,44 +450,28 @@ void ModelChecker::print_stats() const
 bool ModelChecker::next_execution()
 {
 	DBG();
+	/* Is this execution a feasible execution that's worth bug-checking? */
+	bool complete = isfinalfeasible() && (is_complete_execution() ||
+			have_bug_reports());
 
-	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+	/* End-of-execution bug checks */
+	if (complete) {
 		if (is_deadlocked())
 			assert_bug("Deadlock detected");
 
 		checkDataRaces();
+	}
 
-		if (DBG_ENABLED() || params.verbose || have_bug_reports()) {
-			print_program_output();
-
-			if (DBG_ENABLED() || params.verbose) {
-				model_print("Earliest divergence point since last feasible execution:\n");
-				if (earliest_diverge)
-					earliest_diverge->print();
-				else
-					model_print("(Not set)\n");
-
-				model_print("\n");
-				print_stats();
-			}
-
-			print_bugs();
-			model_print("\n");
-			print_summary();
-		} else
-			clear_program_output();
+	record_stats();
 
-		earliest_diverge = NULL;
-	} else if (DBG_ENABLED()) {
-		print_program_output();
-		model_print("\n");
-		print_stats();
-		print_summary();
-	} else {
+	/* Output */
+	if (DBG_ENABLED() || params.verbose || have_bug_reports())
+		print_execution(complete);
+	else
 		clear_program_output();
-	}
 
-	record_stats();
+	if (complete)
+		earliest_diverge = NULL;
 
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
diff --git a/model.h b/model.h
index 447c77d7..0d27d5a3 100644
--- a/model.h
+++ b/model.h
@@ -252,6 +252,7 @@ private:
 
 	bool have_bug_reports() const;
 	void print_bugs() const;
+	void print_execution(bool printbugs) const;
 };
 
 extern ModelChecker *model;
-- 
2.34.1