From: Brian Norris Date: Sun, 4 Nov 2012 01:16:45 +0000 (-0700) Subject: main: add maxfuturevalues parameter (-M) X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=174ad8165eeeb78fb4da391be331a26da044641f main: add maxfuturevalues parameter (-M) Not implemented yet --- diff --git a/main.cc b/main.cc index e8d4f9af..12253981 100644 --- a/main.cc +++ b/main.cc @@ -20,6 +20,7 @@ static void param_defaults(struct model_params * params) { params->fairwindow = 0; params->enabledcount = 1; params->bound = 0; + params->maxfuturevalues = 0; } static void print_usage(struct model_params *params) { @@ -33,6 +34,8 @@ static void print_usage(struct model_params *params) { "-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" +"-M Maximum number of future values that can be sent to\n" +" the same read. 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" @@ -42,12 +45,12 @@ static void print_usage(struct model_params *params) { "-e Enabled count. Default: %d\n" "-b Upper length bound. Default: %d\n" "-- Program arguments follow.\n\n", -params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount, params->bound); +params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->fairwindow, params->enabledcount, params->bound); exit(EXIT_SUCCESS); } static void parse_options(struct model_params *params, int *argc, char ***argv) { - const char *shortopts = "hm:s:f:e:b:"; + const char *shortopts = "hm:M:s:f:e:b:"; int opt; bool error = false; while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) { @@ -70,6 +73,9 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) case 'm': params->maxreads = atoi(optarg); break; + case 'M': + params->maxfuturevalues = atoi(optarg); + break; default: /* '?' */ error = true; break; diff --git a/model.h b/model.h index 59a07597..63f45c72 100644 --- a/model.h +++ b/model.h @@ -37,6 +37,10 @@ struct model_params { unsigned int fairwindow; unsigned int enabledcount; unsigned int bound; + + /** @brief Maximum number of future values that can be sent to the same + * read */ + int maxfuturevalues; }; struct PendingFutureValue {