-void real_main() {
- thrd_t user_thread;
- ucontext_t main_context;
-
- model = new ModelChecker();
-
- if (getcontext(&main_context))
- return;
-
- model->set_system_context(&main_context);
-
- do {
- /* Start user program */
- model->add_thread(new Thread(&user_thread, &user_main, NULL));
-
- /* Wait for all threads to complete */
- thread_wait_finish();
- } while (model->next_execution());
-
- delete model;
-
- DEBUG("Exiting\n");
+
+/** The real_main function contains the main model checking loop. */
+
+static void real_main() {
+ thrd_t user_thread;
+ ucontext_t main_context;
+
+ //Create the singleton SnapshotStack object
+ snapshotObject = new SnapshotStack();
+
+ model = new ModelChecker();
+
+ if (getcontext(&main_context))
+ return;
+
+ model->set_system_context(&main_context);
+
+ snapshotObject->snapshotStep(0);
+
+ do {
+ /* Start user program */
+ model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
+
+ /* Wait for all threads to complete */
+ thread_wait_finish();
+ } while (model->next_execution());
+
+ delete model;
+
+ DEBUG("Exiting\n");