From: bdemsky <bdemsky@uci.edu>
Date: Wed, 26 Jun 2019 21:46:48 +0000 (-0700)
Subject: Redo params
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=fb51932df3796f74631573eb3bb9d1b631f5947a;ds=sidebyside

Redo params
---

diff --git a/main.cc b/main.cc
index 0000c118..df6fff68 100644
--- 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 17ea5427..80d8845f 100644
--- 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 595f6fa9..dc325d71 100644
--- 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 db868958..7f749cae 100644
--- 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__ */