add basic parameter handling

diff --git a/main.cc b/main.cc
index 62acd90de18e4e05114b4519af0e707f5f954aa1..9a6c2d8fcadd5e9127a56082f48a682ce0d803c3 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -58,11 +58,19 @@ static void thread_wait_finish(void) {
        while (!thread_system_next());
 }
 
        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;
 
 /** 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();
 
        //Initialize race detector
        initRaceDetector();


@@ -70,7 +78,7 @@ static void real_main() {
        //Create the singleton SnapshotStack object
        snapshotObject = new SnapshotStack();
 
        //Create the singleton SnapshotStack object
        snapshotObject = new SnapshotStack();
 

-       model = new ModelChecker();
+       model = new ModelChecker(params);

 
        if (getcontext(&main_context))
                return;
 
        if (getcontext(&main_context))
                return;


@@ -91,17 +99,13 @@ static void real_main() {
        DEBUG("Exiting\n");
 }
 
        DEBUG("Exiting\n");
 }
 

-int main_numargs;
-char ** main_args;
-

 /**
  * Main function.  Just initializes snapshotting library and the
  * snapshotting library calls the real_main function.
  */
 /**
  * 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);
 
        /* 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 44235e612f28011ed7dbdd8a87e1ffb4d69aab31..71cf14a3ce136202276e941372ae412787848bac 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -15,13 +15,14 @@
 ModelChecker *model;
 
 /** @brief Constructor */
 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),
        /* 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),
        current_action(NULL),
        diverge(NULL),
        nextThread(THREAD_ID_T_NONE),

diff --git a/model.h b/model.h
index 4e4dcf0ff702b9e825646d0dc56407b81cbed38e..e93c4b51f6aa0cf9c12529c6f1220823f63cb380 100644 (file)
--- a/model.h
+++ b/model.h
@@ -23,10 +23,17 @@ class NodeStack;
 class CycleGraph;
 class Promise;
 
 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:
 /** @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 */
        ~ModelChecker();
 
        /** The scheduler to use: tracks the running/ready Threads */


@@ -73,6 +80,8 @@ private:
        modelclock_t used_sequence_numbers;
        int num_executions;
 
        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
        /**
         * Stores the ModelAction for the current thread action.  Call this
         * immediately before switching from user- to system-context to pass