print stats only at end of execution

diff --git a/main.cc b/main.cc
index 10e2d3b93eae2e3c80e4569464e44a9ebb63d17a..f55b98df2a4cbaa66262497fdad58992c8bac5b0 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -130,6 +130,8 @@ static void model_main() {
                model->finish_execution();
        } while (model->next_execution());
 
+       model->print_stats();
+
        delete model;
 
        DEBUG("Exiting\n");

diff --git a/model.cc b/model.cc
index 8dcb6f3ad8e69a0e82ad3991c4425a35f1a24640..0bc2bde830b97780a2647d2c2c8385c7ddaf8b00 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -436,7 +436,6 @@ bool ModelChecker::next_execution()
                checkDataRaces();
                print_bugs();
                model_print("\n");
-               print_stats();
                print_summary();
        } else if (DBG_ENABLED()) {
                model_print("\n");

diff --git a/model.h b/model.h
index 85deb05e911dc33ae7ea1b245625802dbf4c8708..86fa3e6ab901364c1b7f1df2214c568529fe238a 100644 (file)
--- a/model.h
+++ b/model.h
@@ -122,6 +122,7 @@ public:
        void set_assert() {asserted=true;}
        bool is_deadlocked() const;
        bool is_complete_execution() const;
+       void print_stats() const;
 
        /** @brief Alert the model-checker that an incorrectly-ordered
         * synchronization was made */
@@ -246,7 +247,6 @@ private:
        /** @brief The cumulative execution stats */
        struct execution_stats stats;
        void record_stats();
-       void print_stats() const;
 
        bool have_bug_reports() const;
        void print_bugs() const;