params->uninitvalue = 0;
params->maxexecutions = 10;
params->nofork = false;
+ params->threadsnocleanup = false;
}
static void print_usage(const char *program_name, struct model_params *params)
" Default: %u\n"
" -o help for a list of options\n"
"-n No fork\n"
+#ifdef TLS
+ "-d Don't allow threads to cleanup\n"
+#endif
" -- Program arguments follow.\n\n",
program_name,
params->verbose,
static void parse_options(struct model_params *params, int argc, char **argv)
{
- const char *shortopts = "hnt:o:u:x:v::";
+ const char *shortopts = "hdnt:o:u:x:v::";
const struct option longopts[] = {
{"help", no_argument, NULL, 'h'},
{"verbose", optional_argument, NULL, 'v'},
case 'h':
print_usage(argv[0], params);
break;
+ case 'd':
+ params->threadsnocleanup = true;
+ break;
case 'n':
params->nofork = true;
break;
}
}
-/** The model_main function contains the main model checking loop. */
-static void model_main()
-{
- snapshot_record(0);
- model->run();
- delete model;
-
- DEBUG("Exiting\n");
-}
-
/**
* Main function. Just initializes snapshotting library and the
* snapshotting library calls the model_main function.
main_argv = argv;
/*
- * If this printf statement is removed, CDSChecker will fail on an
+ * If this printf statement is removed, C11Tester will fail on an
* assert on some versions of glibc. The first time printf is
* called, it allocated internal buffers. We can't easily snapshot
* libc since we also use it.
*/
- printf("CDSChecker\n"
- "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
+ printf("C11Tester\n"
+ "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
"Distributed under the GPLv2\n"
- "Written by Brian Norris and Brian Demsky\n\n");
+ "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
- /* Configure output redirection for the model-checker */
- redirect_output();
//Initialize snapshotting library and model checker object
if (!model) {
snapshot_system_init(10000, 1024, 1024, 40000);
model = new ModelChecker();
+ model->startChecker();
}
+ /* Configure output redirection for the model-checker */
+ redirect_output();
+
register_plugins();
//Parse command line options
model_params *params = model->getParams();
parse_options(params, main_argc, main_argv);
- //Initialize race detector
- initRaceDetector();
- snapshot_stack_init();
install_trace_analyses(model->get_execution());
- //Start everything up
- modelchecker_started = true;
- startExecution(&model_main);
+ model->startMainThread();
+ DEBUG("Exiting\n");
}