From: Brian Norris <banorris@uci.edu>
Date: Thu, 2 Aug 2012 18:13:46 +0000 (-0700)
Subject: model: do not call isfinalfeasible() too many times
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7cee72d776ddfbf585038f3cad3df799e353cc11;p=c11tester.git

model: do not call isfinalfeasible() too many times

This function call incurs graph exploration, so when performing some
end-of-trace bookkeeping, we should only call it once and cache the result.
---

diff --git a/model.cc b/model.cc
index 98c6e645..4844c566 100644
--- a/model.cc
+++ b/model.cc
@@ -171,8 +171,9 @@ bool ModelChecker::next_execution()
 
 	num_executions++;
 
-	if (isfinalfeasible() || DBG_ENABLED())
-		print_summary();
+	bool feasible = isfinalfeasible();
+	if (feasible || DBG_ENABLED())
+		print_summary(feasible);
 
 	if ((diverge = model->get_next_backtrack()) == NULL)
 		return false;
@@ -704,7 +705,7 @@ static void print_list(action_list_t *list)
 	printf("---------------------------------------------------------------------\n");
 }
 
-void ModelChecker::print_summary(void)
+void ModelChecker::print_summary(bool feasible)
 {
 	printf("\n");
 	printf("Number of executions: %d\n", num_executions);
@@ -712,7 +713,7 @@ void ModelChecker::print_summary(void)
 
 	scheduler->print();
 
-	if (!isfinalfeasible())
+	if (!feasible)
 		printf("INFEASIBLE EXECUTION!\n");
 	print_list(action_trace);
 	printf("\n");
diff --git a/model.h b/model.h
index 4a55c52b..4e4dcf0f 100644
--- a/model.h
+++ b/model.h
@@ -42,7 +42,14 @@ public:
 	ucontext_t * get_system_context(void) { return system_context; }
 
 	void check_current_action(void);
-	void print_summary(void);
+
+	/**
+	 * Prints an execution summary with trace information.
+	 * @param feasible Formats outputting according to whether or not the
+	 * current trace is feasible. Defaults to feasible = true.
+	 */
+	void print_summary(bool feasible = true);
+
 	Thread * schedule_next_thread();
 
 	int add_thread(Thread *t);