From: Brian Norris <banorris@uci.edu>
Date: Sat, 17 Nov 2012 08:01:18 +0000 (-0800)
Subject: model: add "# redundant" stat
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=f71df291f0158236d46fc39e9c5ca02e3329f628;ds=sidebyside

model: add "# redundant" stat
---

diff --git a/model.cc b/model.cc
index eb5cd347..df067608 100644
--- a/model.cc
+++ b/model.cc
@@ -401,12 +401,15 @@ void ModelChecker::record_stats()
 		stats.num_buggy_executions++;
 	else if (is_complete_execution())
 		stats.num_complete++;
+	else
+		stats.num_redundant++;
 }
 
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {
 	model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+	model_print("Number of redundant executions: %d\n", stats.num_redundant);
 	model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
 	model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
 	model_print("Total executions: %d\n", stats.num_total);
diff --git a/model.h b/model.h
index 0d27d5a3..15516e26 100644
--- a/model.h
+++ b/model.h
@@ -58,6 +58,7 @@ struct execution_stats {
 	int num_infeasible; /**< @brief Number of infeasible executions */
 	int num_buggy_executions; /** @brief Number of buggy executions */
 	int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
+	int num_redundant; /**< @brief Number of redundant, aborted executions */
 };
 
 struct PendingFutureValue {