From ea4611c1fc3b580020afbc04d531e4bc10fcca9c Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 6 Mar 2013 19:17:58 -0800 Subject: [PATCH] add new option for uninitialized writes... --- main.cc | 9 +++++++-- model.cc | 2 +- model.h | 1 + 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/main.cc b/main.cc index d69e9e0..ab37af4 100644 --- a/main.cc +++ b/main.cc @@ -24,6 +24,7 @@ static void param_defaults(struct model_params *params) params->maxfuturevalues = 0; params->expireslop = 10; params->verbose = !!DBG_ENABLED(); + params->uninitvalue = 0; } static void print_usage(struct model_params *params) @@ -52,14 +53,15 @@ static void print_usage(struct model_params *params) "-e Enabled count. Default: %d\n" "-b Upper length bound. Default: %d\n" "-v Print verbose execution information.\n" +"-u Value for uninitialized reads. Default: %u\n" "-- Program arguments follow.\n\n", -params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound); +params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound, params->uninitvalue); exit(EXIT_SUCCESS); } static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hym:M:s:S:f:e:b:v"; + const char *shortopts = "hym:M:s:S:f:e:b:u:v"; int opt; bool error = false; while (!error && (opt = getopt(argc, argv, shortopts)) != -1) { @@ -91,6 +93,9 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'v': params->verbose = 1; break; + case 'u': + params->uninitvalue = atoi(optarg); + break; case 'y': params->yieldon = true; break; diff --git a/model.cc b/model.cc index d2a2c74..0122922 100644 --- a/model.cc +++ b/model.cc @@ -2827,7 +2827,7 @@ ModelAction * ModelChecker::get_uninitialized_action(const ModelAction *curr) co Node *node = curr->get_node(); ModelAction *act = node->get_uninit_action(); if (!act) { - act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), 0, model_thread); + act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), model->params.uninitvalue, model_thread); node->set_uninit_action(act); } act->create_cv(NULL); diff --git a/model.h b/model.h index ae9706b..96c1ec7 100644 --- a/model.h +++ b/model.h @@ -42,6 +42,7 @@ struct model_params { unsigned int fairwindow; unsigned int enabledcount; unsigned int bound; + unsigned int uninitvalue; /** @brief Maximum number of future values that can be sent to the same * read */ -- 2.34.1