add basic parameter handling
authorBrian Norris <banorris@uci.edu>
Wed, 8 Aug 2012 22:22:25 +0000 (15:22 -0700)
committerBrian Norris <banorris@uci.edu>
Sat, 11 Aug 2012 00:24:06 +0000 (17:24 -0700)
main.cc
model.cc
model.h

diff --git a/main.cc b/main.cc
index 62acd90..9a6c2d8 100644 (file)
--- 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(&params, 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);
index 44235e6..71cf14a 100644 (file)
--- a/model.cc
+++ b/model.cc
 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 (file)
--- 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