more bug fixes
authorbdemsky <bdemsky@uci.edu>
Wed, 26 Jun 2019 20:18:06 +0000 (13:18 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 26 Jun 2019 20:18:06 +0000 (13:18 -0700)
cmodelint.cc
main.cc
model.cc
model.h
pthread.cc

index 96cd1c4..7755913 100644 (file)
@@ -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 cc3fcbf..0000c11 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());
index c468d0d..17ea542 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 46c2454..595f6fa 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__ */
index 79e9042..808aa20 100644 (file)
@@ -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;