X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=main.cc;h=31184fc559e6a6dc524f47bd58e60f8c7920c21e;hb=cdf3ae3d7205018a412f75addf4113587a1a0586;hp=75efafed43870f8be079fc8fcb1cb49bd8412706;hpb=3519c47202090f3c4a69de0e89aaa2617b17ff75;p=model-checker.git diff --git a/main.cc b/main.cc index 75efafe..31184fc 100644 --- a/main.cc +++ b/main.cc @@ -2,6 +2,8 @@ * @brief Entry point for the model checker. */ +#include + #include "libthreads.h" #include "common.h" #include "threads.h" @@ -12,7 +14,52 @@ #include "model.h" #include "snapshot-interface.h" -static void parse_options(struct model_params *params, int argc, char **argv) { +static void param_defaults(struct model_params * params) { + params->maxreads = 0; + params->maxfuturedelay = 100; +} + +static void print_usage(struct model_params *params) { + printf( +"Usage: [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n" +"\n" +"Options:\n" +"-h Display this help message and exit\n" +"-m Maximum times a thread can read from the same write\n" +" while other writes exist. Default: %d\n" +"-s Maximum actions that the model checker will wait for\n" +" a write from the future past the expected number of\n" +" actions. Default: %d\n" +"-- Program arguments follow.\n\n", + params->maxreads, params->maxfuturedelay); + exit(EXIT_SUCCESS); +} + +static void parse_options(struct model_params *params, int *argc, char ***argv) { + const char *shortopts = "hm:s:"; + int opt; + bool error = false; + while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) { + switch (opt) { + case 'h': + print_usage(params); + break; + case 's': + params->maxfuturedelay = atoi(optarg); + break; + case 'm': + params->maxreads = atoi(optarg); + break; + default: /* '?' */ + error = true; + break; + } + } + (*argc) -= optind; + (*argv) += optind; + + if (error) + print_usage(params); } int main_argc; @@ -23,7 +70,9 @@ static void real_main() { thrd_t user_thread; struct model_params params; - parse_options(¶ms, main_argc, main_argv); + param_defaults(¶ms); + + parse_options(¶ms, &main_argc, &main_argv); //Initialize race detector initRaceDetector();