X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=5a33baf996bc3d0f85f11108797b8907c89b6507;hb=f817fff71c1cc97fe1bd55fa791f0d68af88ed1a;hp=c8417c027666219b9fdaa6da21d256ad4ebdf42c;hpb=b090a4abc4915a9aa2a29787f76a6add79f838e2;p=model-checker.git diff --git a/main.cc b/main.cc index c8417c0..5a33baf 100644 --- a/main.cc +++ b/main.cc @@ -35,6 +35,7 @@ static void param_defaults(struct model_params *params) static void print_usage(const char *program_name, struct model_params *params) { + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); /* Reset defaults before printing */ param_defaults(params); @@ -78,7 +79,9 @@ static void print_usage(const char *program_name, struct model_params *params) "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n" " uninitialized atomic.\n" " Default: %u\n" -"-t, --analysis=NAME Use Trace Analysis.\n" +"-t, --analysis=NAME Use Analysis Plugin.\n" +"-o, --options=NAME Option for previous analysis plugin. \n" +" -o help for a list of options\n" " -- Program arguments follow.\n\n", program_name, params->maxreads, @@ -91,6 +94,11 @@ static void print_usage(const char *program_name, struct model_params *params) params->enabledcount, params->bound, params->uninitvalue); + model_print("Analysis plug ins:\n"); + for(unsigned int i=0;isize();i++) { + TraceAnalysis * analysis=(*registeredanalysis)[i]; + model_print("%s\n", analysis->name()); + } exit(EXIT_SUCCESS); } @@ -111,7 +119,7 @@ bool install_plugin(char * name) { static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hyYt:m:M:s:S:f:e:b:u:v::"; + const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"liveness", required_argument, NULL, 'm'}, @@ -126,6 +134,7 @@ static void parse_options(struct model_params *params, int argc, char **argv) {"verbose", optional_argument, NULL, 'v'}, {"uninitialized", optional_argument, NULL, 'u'}, {"analysis", optional_argument, NULL, 't'}, + {"options", optional_argument, NULL, 'o'}, {0, 0, 0, 0} /* Terminator */ }; int opt, longindex; @@ -169,6 +178,13 @@ static void parse_options(struct model_params *params, int argc, char **argv) if (install_plugin(optarg)) error = true; break; + case 'o': + { + ModelVector * analyses = getInstalledTraceAnalysis(); + if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg)) + error = true; + } + break; case 'Y': params->yieldblock = true; break;