X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=dc3f6f4dca002d6e763e5bbf25068260d3edc828;hb=dc9c89654982c64264dfee7b1ea23e9a5e88e18e;hp=bc8a08ec6f05b5c7848feb6d8d474db793add8b0;hpb=4b03f676b719a8e10990f33d746ce5dd94d1337d;p=model-checker.git diff --git a/main.cc b/main.cc index bc8a08e..dc3f6f4 100644 --- a/main.cc +++ b/main.cc @@ -13,7 +13,8 @@ #include "model.h" #include "snapshot-interface.h" -static void param_defaults(struct model_params * params) { +static void param_defaults(struct model_params *params) +{ params->maxreads = 0; params->maxfuturedelay = 100; params->fairwindow = 0; @@ -24,7 +25,8 @@ static void param_defaults(struct model_params * params) { params->verbose = 0; } -static void print_usage(struct model_params *params) { +static void print_usage(struct model_params *params) +{ /* Reset defaults before printing */ param_defaults(params); @@ -52,7 +54,8 @@ params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expir exit(EXIT_SUCCESS); } -static void parse_options(struct model_params *params, int argc, char **argv) { +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; @@ -109,7 +112,8 @@ int main_argc; char **main_argv; /** The model_main function contains the main model checking loop. */ -static void model_main() { +static void model_main() +{ struct model_params params; param_defaults(¶ms); @@ -119,11 +123,10 @@ static void model_main() { //Initialize race detector initRaceDetector(); - //Create the singleton SnapshotStack object - snapshotObject = new SnapshotStack(); + snapshot_stack_init(); model = new ModelChecker(params); - snapshotObject->snapshotStep(0); + snapshot_record(0); model->run(); delete model; @@ -134,7 +137,8 @@ static void model_main() { * Main function. Just initializes snapshotting library and the * snapshotting library calls the model_main function. */ -int main(int argc, char ** argv) { +int main(int argc, char **argv) +{ main_argc = argc; main_argv = argv; @@ -142,5 +146,5 @@ int main(int argc, char ** argv) { redirect_output(); /* Let's jump in quickly and start running stuff */ - initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main); + snapshot_system_init(10000, 1024, 1024, 4000, &model_main); }