ta->actionAtInstallation();
}
}
-
-/**
- * Main function. Just initializes snapshotting library and the
- * snapshotting library calls the model_main function.
- */
-int main(int argc, char **argv)
-{
- /*
- * 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("C11Tester\n"
- "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
- "Distributed under the GPLv2\n"
- "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
-
-
- //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();
-
- //Stash command line options
- model_params *params = model->getParams();
- params->argc = argc;
- params->argv = argv;
-
- install_trace_analyses(model->get_execution());
-
- model->startMainThread();
- DEBUG("Exiting\n");
-}
ModelChecker *model = NULL;
-/** 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 Constructor */
ModelChecker::ModelChecker() :
/* Initialize default scheduler */
trace_analyses(),
inspect_plugin(NULL)
{
+ 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 Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
memset(&stats,0,sizeof(struct execution_stats));
- init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), NULL, NULL, NULL);
#ifdef TLS
init_thread->setTLS((char *)get_tls_addr());
#endif
execution->add_thread(init_thread);
scheduler->set_current_thread(init_thread);
+ register_plugins();
execution->setParams(¶ms);
param_defaults(¶ms);
parse_options(¶ms);
initRaceDetector();
+ /* Configure output redirection for the model-checker */
+ redirect_output();
+ install_trace_analyses(model->get_execution());
}
/** @brief Destructor */
/** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
int verbose;
-
- /** @brief Command-line argument count to pass to user program */
- int argc;
-
- /** @brief Command-line arguments to pass to user program */
- char **argv;
};
void param_defaults(struct model_params *params);