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;
"Distributed under the GPLv2\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) {
model->startChecker();
}
+ /* Configure output redirection for the model-checker */
+ redirect_output();
+
register_plugins();
//Parse command line options
parse_options(params, main_argc, main_argv);
- snapshot_stack_init();
install_trace_analyses(model->get_execution());
- snapshot_record(0);
model->startMainThread();
DEBUG("Exiting\n");
}