From 4cf371ec71d080e89bd6f4c3385c97a1b752e9f6 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 26 Jun 2019 13:18:06 -0700
Subject: [PATCH] more bug fixes

---
 cmodelint.cc |  8 ++++----
 main.cc      |  7 +++----
 model.cc     |  2 +-
 model.h      |  3 +--
 pthread.cc   | 13 +++++--------
 5 files changed, 14 insertions(+), 19 deletions(-)

diff --git a/cmodelint.cc b/cmodelint.cc
index 96cd1c49..77559136 100644
--- 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 cc3fcbf0..0000c118 100644
--- 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 c468d0de..17ea5427 100644
--- 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 46c24543..595f6fa9 100644
--- 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 79e90425..808aa207 100644
--- 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;
-- 
2.34.1