1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
5 * This program is free software; you can redistribute it and/or
6 * modify it under the terms of the GNU General Public License
7 * version 2 as published by the Free Software Foundation.
11 #include "snapshot-interface.h"
12 #include "mcschedule.h"
18 MC::MC(struct model_params params) :
20 execution(new MCExecution())
28 /** Wrapper to run the user's main function, with appropriate arguments */
29 void user_main_wrapper(void *) {
30 user_main(model->params.argc, model->params.argv);
33 /** Implements the main loop for model checking test case
39 execution->get_planner()->plan();
40 print_program_output();
41 #if SUPPORT_MOD_ORDER_DUMP
42 execution->dumpExecution();
45 snapshot_backtrack_before(0);
46 } while(!execution->get_planner()->is_finished());
47 dprintf(2, "Finished!\n");
51 /** Executes a single execution. */
53 void MC::run_execution() {
55 Thread *t = new Thread(execution->get_next_tid(), &user_thread, &user_main_wrapper, NULL, NULL, NULL);
56 execution->add_thread(t);
57 execution->get_scheduler()->swap_threads(NULL, t);