model: refactor end-of-execution output

diff --git a/model.cc b/model.cc
index 691cd72bbbbd5275473ddf0993f70138256a0f0b..eb5cd347e0442d60cdd35fea377afe189cea2177 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -413,6 +413,33 @@ void ModelChecker::print_stats() const
        model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
 }
 
+/**
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
+ */
+void ModelChecker::print_execution(bool printbugs) const
+{
+       print_program_output();
+
+       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");
+
+               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.
@@ -423,44 +450,28 @@ void ModelChecker::print_stats() const
 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());
 
-       if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+       /* End-of-execution bug checks */
+       if (complete) {
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
+       }
 
-               if (DBG_ENABLED() || params.verbose || have_bug_reports()) {
-                       print_program_output();
-
-                       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");
-
-                               model_print("\n");
-                               print_stats();
-                       }
-
-                       print_bugs();
-                       model_print("\n");
-                       print_summary();
-               } else
-                       clear_program_output();
+       record_stats();
 
-               earliest_diverge = NULL;
-       } else if (DBG_ENABLED()) {
-               print_program_output();
-               model_print("\n");
-               print_stats();
-               print_summary();
-       } else {
+       /* Output */
+       if (DBG_ENABLED() || params.verbose || have_bug_reports())
+               print_execution(complete);
+       else
                clear_program_output();
-       }
 
-       record_stats();
+       if (complete)
+               earliest_diverge = NULL;
 
        if ((diverge = get_next_backtrack()) == NULL)
                return false;

diff --git a/model.h b/model.h
index 447c77d74e56c01781d415ee95bd0a1a7b76b74a..0d27d5a305d1830b75ac3519e294816f85bc88de 100644 (file)
--- a/model.h
+++ b/model.h
@@ -252,6 +252,7 @@ private:
 
        bool have_bug_reports() const;
        void print_bugs() const;
+       void print_execution(bool printbugs) const;
 };
 
 extern ModelChecker *model;