Redo params

diff --git a/main.cc b/main.cc
index 0000c118ba91bb58c3918d264bb1a7a7d49a2206..df6fff6856ad484013f6386950a869b4727e8607 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -17,7 +17,7 @@
 #include "snapshot-interface.h"
 #include "plugins.h"
 
-static void param_defaults(struct model_params *params)
+void param_defaults(struct model_params *params)
 {
        params->verbose = !!DBG_ENABLED();
        params->uninitvalue = 0;
@@ -164,7 +164,6 @@ static void install_trace_analyses(ModelExecution *execution)
 /** The model_main function contains the main model checking loop. */
 static void model_main()
 {
-       modelchecker_started = true;
        snapshot_record(0);
        model->run();
        delete model;
@@ -196,26 +195,25 @@ int main(int argc, char **argv)
        /* Configure output redirection for the model-checker */
        redirect_output();
 
-       //Initialize snapshotting library
-       if (!model)
+       //Initialize snapshotting library and model checker object
+       if (!model) {
                snapshot_system_init(10000, 1024, 1024, 40000);
+               model = new ModelChecker();
+       }
 
-       struct model_params params;
-
-       param_defaults(&params);
        register_plugins();
-       parse_options(&params, main_argc, main_argv);
+
+       //Parse command line options
+       model_params *params = model->getParams();
+       parse_options(params, main_argc, main_argv);
 
        //Initialize race detector
        initRaceDetector();
 
        snapshot_stack_init();
-
-       if (!model)
-               model = new ModelChecker();
-
-       model->setParams(params);
        install_trace_analyses(model->get_execution());
 
+       //Start everything up
+       modelchecker_started = true;
        startExecution(&model_main);
 }

diff --git a/model.cc b/model.cc
index 17ea5427d70bd19d8a0cd9856a9a997e077f3162..80d8845fed99714d9ba1dcd93cab9f40efcc5806 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -17,6 +17,7 @@
 #include "traceanalysis.h"
 #include "execution.h"
 #include "bugmessage.h"
+#include "params.h"
 
 ModelChecker *model = NULL;
 bool modelchecker_started = false;
@@ -43,6 +44,8 @@ ModelChecker::ModelChecker() :
        init_thread = new Thread(execution->get_next_id(), (thrd_t *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);  // L: user_main_wrapper passes the user program
        execution->add_thread(init_thread);
        scheduler->set_current_thread(init_thread);
+       execution->setParams(&params);
+       param_defaults(&params);
 }
 
 /** @brief Destructor */
@@ -53,9 +56,8 @@ ModelChecker::~ModelChecker()
 }
 
 /** Method to set parameters */
-void ModelChecker::setParams(struct model_params params) {
-       this->params = params;
-       execution->setParams(&params);
+model_params * ModelChecker::getParams() {
+       return &params;
 }
 
 /**

diff --git a/model.h b/model.h
index 595f6fa9d7d139af378584974d5fcc5e433fb0a0..dc325d71744398e28b75d2cfa0929c34d78e9cc8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -33,7 +33,7 @@ class ModelChecker {
 public:
        ModelChecker();
        ~ModelChecker();
-       void setParams(struct model_params params);
+       model_params * getParams();
        void run();
 
        /** Restart the model checker, intended for pluggins. */

diff --git a/params.h b/params.h
index db86895890d8061cbe4fedbc04d908263c5081be..7f749cae6fc082d1551fdfb86f0c5728cf176fbc 100644 (file)
--- a/params.h
+++ b/params.h
@@ -20,4 +20,6 @@ struct model_params {
        char **argv;
 };
 
+void param_defaults(struct model_params *params);
+
 #endif /* __PARAMS_H__ */