X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=9ed6d423452a52e5c4ee006fa624fad809bdebc3;hp=0bc2bde830b97780a2647d2c2c8385c7ddaf8b00;hb=80f5924fb6c148ecb703dfeae5a751948062588b;hpb=e83585ce14ab6ae325c83d815dce8eb77b0e5897

diff --git a/model.cc b/model.cc
index 0bc2bde8..9ed6d423 100644
--- a/model.cc
+++ b/model.cc
@@ -13,6 +13,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "threads-model.h"
+#include "output.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -139,6 +140,10 @@ void ModelChecker::reset_to_initial_state()
 	too_many_reads = false;
 	bad_synchronization = false;
 	reset_asserted();
+
+	/* Print all model-checker output before rollback */
+	fflush(model_out);
+
 	snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -419,8 +424,6 @@ bool ModelChecker::next_execution()
 {
 	DBG();
 
-	record_stats();
-
 	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
 		model_print("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
@@ -442,6 +445,8 @@ bool ModelChecker::next_execution()
 		print_summary();
 	}
 
+	record_stats();
+
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
 
@@ -2221,12 +2226,14 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
 	}
 }
 
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
 {
 	action_list_t::iterator it;
 
 	model_print("---------------------------------------------------------------------\n");
-	model_print("Trace:\n");
+	if (exec_num >= 0)
+		model_print("Execution %d:\n", exec_num);
+
 	unsigned int hash=0;
 
 	for (it = list->begin(); it != list->end(); it++) {
@@ -2278,7 +2285,7 @@ void ModelChecker::print_summary()
 
 	if (!isfinalfeasible())
 		model_print("INFEASIBLE EXECUTION!\n");
-	print_list(action_trace);
+	print_list(action_trace, stats.num_total);
 	model_print("\n");
 }