main/model: move full user-program execution to ModelChecker::run

We don't really need the top-level ModelChecker execution loop to be in
main.cc; it should be exposed simply as a run() method.

diff --git a/main.cc b/main.cc
index a577ed2b43b1268c96a74f011702876f316ea9b5..64564012fa634f6281ee7d6834facd2ce4dc3da4 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -104,15 +104,8 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
 int main_argc;
 char **main_argv;
 
-/** Wrapper to run the user's main function, with appropriate arguments */
-void wrapper_user_main(void *)
-{
-       user_main(main_argc, main_argv);
-}
-
 /** The model_main function contains the main model checking loop. */
 static void model_main() {
-       thrd_t user_thread;
        struct model_params params;
 
        param_defaults(&params);
@@ -130,18 +123,8 @@ static void model_main() {
        snapshotObject = new SnapshotStack();
 
        model = new ModelChecker(params);
-
        snapshotObject->snapshotStep(0);
-       do {
-               /* Start user program */
-               model->add_thread(new Thread(&user_thread, &wrapper_user_main, NULL));
-
-               /* Wait for all threads to complete */
-               model->finish_execution();
-       } while (model->next_execution());
-
-       model->print_stats();
-
+       model->run();
        delete model;
 
        DEBUG("Exiting\n");

diff --git a/model.cc b/model.cc
index fd893c78b42a85cec0bc2668102600f1a4fa63c8..43700989ad530a057fdcd70f45f30ad2b01f147e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2516,3 +2516,25 @@ void ModelChecker::finish_execution() {
 
        while (take_step());
 }
+
+/** Wrapper to run the user's main function, with appropriate arguments */
+void user_main_wrapper(void *)
+{
+       user_main(model->params.argc, model->params.argv);
+}
+
+/** @brief Run ModelChecker for the user program */
+void ModelChecker::run()
+{
+       do {
+               thrd_t user_thread;
+
+               /* Start user program */
+               add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+
+               /* Wait for all threads to complete */
+               finish_execution();
+       } while (next_execution());
+
+       print_stats();
+}

diff --git a/model.h b/model.h
index 04e191bed53340819ee1fa87c326bf9bcfbc89a6..5f389c5b9d245d359434772240e7212a27c7c8ba 100644 (file)
--- a/model.h
+++ b/model.h
@@ -91,6 +91,8 @@ public:
        ModelChecker(struct model_params params);
        ~ModelChecker();
 
+       void run();
+
        /** @returns the context for the main model-checking system thread */
        ucontext_t * get_system_context() { return &system_context; }
 
@@ -252,6 +254,8 @@ private:
        bool have_bug_reports() const;
        void print_bugs() const;
        void print_execution(bool printbugs) const;
+
+       friend void user_main_wrapper();
 };
 
 extern ModelChecker *model;