-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);
-
- 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());
-
+static void parse_options(struct model_params *params, int argc, char **argv)
+{
+ const char *shortopts = "hm:M:s:S:f:e:b:v";
+ int opt;
+ bool error = false;
+ while (!error && (opt = getopt(argc, argv, shortopts)) != -1) {
+ switch (opt) {
+ case 'h':
+ print_usage(params);
+ break;
+ case 's':
+ params->maxfuturedelay = atoi(optarg);
+ break;
+ case 'S':
+ params->expireslop = atoi(optarg);
+ break;
+ case 'f':
+ params->fairwindow = atoi(optarg);
+ break;
+ case 'e':
+ params->enabledcount = atoi(optarg);
+ break;
+ case 'b':
+ params->bound = atoi(optarg);
+ break;
+ case 'm':
+ params->maxreads = atoi(optarg);
+ break;
+ case 'M':
+ params->maxfuturevalues = atoi(optarg);
+ break;
+ case 'v':
+ params->verbose = 1;
+ break;
+ default: /* '?' */
+ error = true;
+ break;
+ }
+ }
+
+ /* Pass remaining arguments to user program */
+ params->argc = argc - (optind - 1);
+ params->argv = argv + (optind - 1);
+
+ /* Reset program name */
+ params->argv[0] = argv[0];
+
+ /* Reset (global) optind for potential use by user program */
+ optind = 1;
+
+ if (error)
+ print_usage(params);
+}
+
+int main_argc;
+char **main_argv;
+
+/** The model_main function contains the main model checking loop. */
+static void model_main()
+{
+ struct model_params params;
+
+ param_defaults(¶ms);
+
+ parse_options(¶ms, main_argc, main_argv);
+
+ //Initialize race detector
+ initRaceDetector();
+
+ snapshot_stack_init();
+
+ model = new ModelChecker(params);
+ snapshot_record(0);
+ model->run();