From 508af0435527c006aceeed751abe0b4daa73e27e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 8 Aug 2012 15:22:25 -0700 Subject: [PATCH] add basic parameter handling --- main.cc | 20 ++++++++++++-------- model.cc | 3 ++- model.h | 11 ++++++++++- 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/main.cc b/main.cc index 62acd90..9a6c2d8 100644 --- a/main.cc +++ b/main.cc @@ -58,11 +58,19 @@ static void thread_wait_finish(void) { while (!thread_system_next()); } +static void parse_options(struct model_params *params, int argc, char **argv) { +} + +int main_argc; +char **main_argv; /** The real_main function contains the main model checking loop. */ static void real_main() { thrd_t user_thread; ucontext_t main_context; + struct model_params params; + + parse_options(¶ms, main_argc, main_argv); //Initialize race detector initRaceDetector(); @@ -70,7 +78,7 @@ static void real_main() { //Create the singleton SnapshotStack object snapshotObject = new SnapshotStack(); - model = new ModelChecker(); + model = new ModelChecker(params); if (getcontext(&main_context)) return; @@ -91,17 +99,13 @@ static void real_main() { DEBUG("Exiting\n"); } -int main_numargs; -char ** main_args; - /** * Main function. Just initializes snapshotting library and the * snapshotting library calls the real_main function. */ -int main(int numargs, char ** args) { - /* Stash this stuff in case someone wants it eventually */ - main_numargs=numargs; - main_args=args; +int main(int argc, char ** argv) { + main_argc = argc; + main_argv = argv; /* Let's jump in quickly and start running stuff */ initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main); diff --git a/model.cc b/model.cc index 44235e6..71cf14a 100644 --- a/model.cc +++ b/model.cc @@ -15,13 +15,14 @@ ModelChecker *model; /** @brief Constructor */ -ModelChecker::ModelChecker() : +ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ scheduler(new Scheduler()), /* First thread created will have id INITIAL_THREAD_ID */ next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), num_executions(0), + params(params), current_action(NULL), diverge(NULL), nextThread(THREAD_ID_T_NONE), diff --git a/model.h b/model.h index 4e4dcf0..e93c4b5 100644 --- a/model.h +++ b/model.h @@ -23,10 +23,17 @@ class NodeStack; class CycleGraph; class Promise; +/** + * Model checker parameter structure. Holds run-time configuration options for + * the model checker. + */ +struct model_params { +}; + /** @brief The central structure for model-checking */ class ModelChecker { public: - ModelChecker(); + ModelChecker(struct model_params params); ~ModelChecker(); /** The scheduler to use: tracks the running/ready Threads */ @@ -73,6 +80,8 @@ private: modelclock_t used_sequence_numbers; int num_executions; + const model_params params; + /** * Stores the ModelAction for the current thread action. Call this * immediately before switching from user- to system-context to pass -- 2.34.1