X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=56eb311dd86f755d45989972d1fe165be74c60a2;hb=a6ce579c6437ebead8fee2c8df1530d223591318;hp=fa7075408f7d16c8bf92a00abfb13b0e0c878d5d;hpb=4541dc5155c69e168beedf3bd2a8f5ece0e0e65b;p=model-checker.git diff --git a/main.cc b/main.cc index fa70754..56eb311 100644 --- a/main.cc +++ b/main.cc @@ -11,6 +11,7 @@ /* global "model" object */ #include "model.h" +#include "params.h" #include "snapshot-interface.h" #include "scanalysis.h" @@ -68,7 +69,7 @@ params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expir static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hymc:M:s:S:f:e:b:u:v"; + const char *shortopts = "hycm:M:s:S:f:e:b:u:v"; int opt; bool error = false; while (!error && (opt = getopt(argc, argv, shortopts)) != -1) { @@ -132,9 +133,10 @@ static void parse_options(struct model_params *params, int argc, char **argv) int main_argc; char **main_argv; -void install_trace_analyses() { +static void install_trace_analyses(const ModelExecution *execution) +{ if (model->params.sc_trace_analysis) - model->add_trace_analysis(new SCAnalysis()); + model->add_trace_analysis(new SCAnalysis(execution)); } /** The model_main function contains the main model checking loop. */ @@ -152,7 +154,7 @@ static void model_main() snapshot_stack_init(); model = new ModelChecker(params); - install_trace_analyses(); + install_trace_analyses(model->get_execution()); snapshot_record(0); model->run();