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

[model-checker.git] / model.cc

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();
+}