model: add "# redundant" stat

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 9ed6d423452a52e5c4ee006fa624fad809bdebc3..df06760893018d5bc1756cd89df263c6ed117cc6 100644 (file)
--- 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);
@@ -414,39 +417,65 @@ void ModelChecker::print_stats() const
 }
 
 /**
- * Queries the model-checker for more executions to explore and, if one
- * exists, resets the model-checker state to execute a new execution.
- *
- * @return If there are more executions to explore, return true. Otherwise,
- * return false.
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
  */
-bool ModelChecker::next_execution()
+void ModelChecker::print_execution(bool printbugs) const
 {
-       DBG();
+       print_program_output();
 
-       if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+       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");
 
-               earliest_diverge = NULL;
+               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.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
+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());
 
+       /* End-of-execution bug checks */
+       if (complete) {
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
-               print_bugs();
-               model_print("\n");
-               print_summary();
-       } else if (DBG_ENABLED()) {
-               model_print("\n");
-               print_summary();
        }
 
        record_stats();
 
+       /* Output */
+       if (DBG_ENABLED() || params.verbose || have_bug_reports())
+               print_execution(complete);
+       else
+               clear_program_output();
+
+       if (complete)
+               earliest_diverge = NULL;
+
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
@@ -2272,7 +2301,8 @@ void ModelChecker::dumpGraph(char *filename) {
 }
 #endif
 
-void ModelChecker::print_summary()
+/** @brief Prints an execution trace summary. */
+void ModelChecker::print_summary() const
 {
 #if SUPPORT_MOD_ORDER_DUMP
        scheduler->print();