From fb6d374952284313141eaee75ecd322209d152db Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 31 May 2013 16:50:40 -0700
Subject: [PATCH 1/1] model: cosmetic output improvements

A few cosmetic improvements:

* Provide more uniform newlines

* Clearly show which output is produced by the test program

* Provide clear heading to show which output belongs to which program
  execution

* Label the program trace if it has bugs

I'm sure there's more that could be improved, but that's it for now.
---
 common.cc    |  4 ++++
 execution.cc | 10 +++++++---
 model.cc     | 24 +++++++++++++-----------
 3 files changed, 24 insertions(+), 14 deletions(-)

diff --git a/common.cc b/common.cc
index 66b563a..26f6d5d 100644
--- a/common.cc
+++ b/common.cc
@@ -147,6 +147,8 @@ void print_program_output()
 {
 	char buf[200];
 
+	model_print("---- BEGIN PROGRAM OUTPUT ----\n");
+
 	/* Gather all program output */
 	fflush(stdout);
 
@@ -165,5 +167,7 @@ void print_program_output()
 			ret -= res;
 		}
 	}
+
+	model_print("---- END PROGRAM OUTPUT   ----\n");
 }
 #endif /* ! CONFIG_DEBUG */
diff --git a/execution.cc b/execution.cc
index 403d70f..07866fe 100644
--- a/execution.cc
+++ b/execution.cc
@@ -1389,7 +1389,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 	if (promises.size() != 0)
 		ptr += sprintf(ptr, "[unresolved promise]");
 	if (ptr != buf)
-		model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
+		model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
 }
 
 /**
@@ -2697,17 +2697,21 @@ void ModelExecution::print_summary() const
 	dumpGraph(buffername);
 #endif
 
-	model_print("Execution %d:", get_execution_number());
+	model_print("Execution trace %d:", get_execution_number());
 	if (isfeasibleprefix()) {
 		if (is_yieldblocked())
 			model_print(" YIELD BLOCKED");
 		if (scheduler->all_threads_sleeping())
 			model_print(" SLEEP-SET REDUNDANT");
-		model_print("\n");
+		if (have_bug_reports())
+			model_print(" DETECTED BUG(S)");
 	} else
 		print_infeasibility(" INFEASIBLE");
+	model_print("\n");
+
 	print_list(&action_trace);
 	model_print("\n");
+
 	if (!promises.empty()) {
 		model_print("Pending promises:\n");
 		for (unsigned int i = 0; i < promises.size(); i++) {
diff --git a/model.cc b/model.cc
index 466bf61..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 >= 2) {
-		model_print("Earliest divergence point since last feasible execution:\n");
+		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();
-- 
2.34.1