more bug fixes

diff --git a/cmodelint.cc b/cmodelint.cc
index 96cd1c49ef78f56a1a75eb6da46423fe3504123f..77559136f53ab3cb7d673e906a8cfb2c225233de 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -12,12 +12,12 @@ memory_order orders[6] = {
 };
 
 static void ensureModel(ModelAction * action) {
-       if (!model) {
-               if (!model_init) {
+       if (!modelchecker_started) {
+               if (!model) {
                        snapshot_system_init(10000, 1024, 1024, 40000);
-                       model_init = new ModelChecker();
+                       model = new ModelChecker();
                }
-               model_init->get_execution()->check_current_action(action);
+               model->get_execution()->check_current_action(action);
        } else {
                model->switch_to_master(action);
        }

diff --git a/main.cc b/main.cc
index cc3fcbf081316cf3958cf1f59915e4b3ca8d9e9a..0000c118ba91bb58c3918d264bb1a7a7d49a2206 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -164,6 +164,7 @@ 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,7 +197,7 @@ int main(int argc, char **argv)
        redirect_output();
 
        //Initialize snapshotting library
-       if (!model_init)
+       if (!model)
                snapshot_system_init(10000, 1024, 1024, 40000);
 
        struct model_params params;
@@ -210,10 +211,8 @@ int main(int argc, char **argv)
 
        snapshot_stack_init();
 
-       if (!model_init)
+       if (!model)
                model = new ModelChecker();
-       else
-               model = model_init;
 
        model->setParams(params);
        install_trace_analyses(model->get_execution());

diff --git a/model.cc b/model.cc
index c468d0deb3e8b6972673d3910670e99eff42052f..17ea5427d70bd19d8a0cd9856a9a997e077f3162 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -19,7 +19,7 @@
 #include "bugmessage.h"
 
 ModelChecker *model = NULL;
-ModelChecker *model_init = NULL;
+bool modelchecker_started = false;
 
 /** Wrapper to run the user's main function, with appropriate arguments */
 void user_main_wrapper(void *)

diff --git a/model.h b/model.h
index 46c2454319d94b115381e41ad4248cd197732cef..595f6fa9d7d139af378584974d5fcc5e433fb0a0 100644 (file)
--- a/model.h
+++ b/model.h
@@ -104,6 +104,5 @@ private:
 };
 
 extern ModelChecker *model;
-extern ModelChecker *model_init;
-
+extern bool modelchecker_started;
 #endif /* __MODEL_H__ */

diff --git a/pthread.cc b/pthread.cc
index 79e904257b38ef69973ce4733cb55ab3ed1ce527..808aa207cd72338806932b3afd86c2d5abe367c6 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -49,16 +49,13 @@ void pthread_exit(void *value_ptr) {
 
 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
        cdsc::mutex *m = new cdsc::mutex();
-       ModelExecution *execution;
 
        if (!model) {
-               if (!model_init) {
-                       snapshot_system_init(10000, 1024, 1024, 40000);
-                       model_init = new ModelChecker();
-               }
-               execution = model_init->get_execution();
-       } else
-               execution = model->get_execution();
+               snapshot_system_init(10000, 1024, 1024, 40000);
+               model = new ModelChecker();
+       }
+
+       ModelExecution *execution = model->get_execution();
        execution->getMutexMap()->put(p_mutex, m);
 
        return 0;