model: print_summary() should be const

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 0bc2bde830b97780a2647d2c2c8385c7ddaf8b00..691cd72bbbbd5275473ddf0993f70138256a0f0b 100644 (file)
--- 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,29 +424,44 @@ 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)
-                       earliest_diverge->print();
-               else
-                       model_print("(Not set)\n");
-
-               earliest_diverge = NULL;
-
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
-               print_bugs();
-               model_print("\n");
-               print_summary();
+
+               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();
+
+               earliest_diverge = NULL;
        } else if (DBG_ENABLED()) {
+               print_program_output();
                model_print("\n");
+               print_stats();
                print_summary();
+       } else {
+               clear_program_output();
        }
 
+       record_stats();
+
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
@@ -2221,12 +2241,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++) {
@@ -2265,7 +2287,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();
@@ -2278,7 +2301,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");
 }