From: Brian Norris <banorris@uci.edu>
Date: Wed, 8 Aug 2012 22:22:25 +0000 (-0700)
Subject: add basic parameter handling
X-Git-Tag: pldi2013~281
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=508af0435527c006aceeed751abe0b4daa73e27e;hp=5c4fa9302d72d9782a786838d05f5daf261bedd0;p=model-checker.git

add basic parameter handling
---

diff --git a/main.cc b/main.cc
index 62acd90..9a6c2d8 100644
--- a/main.cc
+++ b/main.cc
@@ -58,11 +58,19 @@ static void thread_wait_finish(void) {
 	while (!thread_system_next());
 }
 
+static void parse_options(struct model_params *params, int argc, char **argv) {
+}
+
+int main_argc;
+char **main_argv;
 
 /** The real_main function contains the main model checking loop. */
 static void real_main() {
 	thrd_t user_thread;
 	ucontext_t main_context;
+	struct model_params params;
+
+	parse_options(&params, main_argc, main_argv);
 
 	//Initialize race detector
 	initRaceDetector();
@@ -70,7 +78,7 @@ static void real_main() {
 	//Create the singleton SnapshotStack object
 	snapshotObject = new SnapshotStack();
 
-	model = new ModelChecker();
+	model = new ModelChecker(params);
 
 	if (getcontext(&main_context))
 		return;
@@ -91,17 +99,13 @@ static void real_main() {
 	DEBUG("Exiting\n");
 }
 
-int main_numargs;
-char ** main_args;
-
 /**
  * Main function.  Just initializes snapshotting library and the
  * snapshotting library calls the real_main function.
  */
-int main(int numargs, char ** args) {
-	/* Stash this stuff in case someone wants it eventually */
-	main_numargs=numargs;
-	main_args=args;
+int main(int argc, char ** argv) {
+	main_argc = argc;
+	main_argv = argv;
 
 	/* Let's jump in quickly and start running stuff */
 	initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main);
diff --git a/model.cc b/model.cc
index 44235e6..71cf14a 100644
--- a/model.cc
+++ b/model.cc
@@ -15,13 +15,14 @@
 ModelChecker *model;
 
 /** @brief Constructor */
-ModelChecker::ModelChecker() :
+ModelChecker::ModelChecker(struct model_params params) :
 	/* Initialize default scheduler */
 	scheduler(new Scheduler()),
 	/* First thread created will have id INITIAL_THREAD_ID */
 	next_thread_id(INITIAL_THREAD_ID),
 	used_sequence_numbers(0),
 	num_executions(0),
+	params(params),
 	current_action(NULL),
 	diverge(NULL),
 	nextThread(THREAD_ID_T_NONE),
diff --git a/model.h b/model.h
index 4e4dcf0..e93c4b5 100644
--- a/model.h
+++ b/model.h
@@ -23,10 +23,17 @@ class NodeStack;
 class CycleGraph;
 class Promise;
 
+/**
+ * Model checker parameter structure. Holds run-time configuration options for
+ * the model checker.
+ */
+struct model_params {
+};
+
 /** @brief The central structure for model-checking */
 class ModelChecker {
 public:
-	ModelChecker();
+	ModelChecker(struct model_params params);
 	~ModelChecker();
 
 	/** The scheduler to use: tracks the running/ready Threads */
@@ -73,6 +80,8 @@ private:
 	modelclock_t used_sequence_numbers;
 	int num_executions;
 
+	const model_params params;
+
 	/**
 	 * Stores the ModelAction for the current thread action.  Call this
 	 * immediately before switching from user- to system-context to pass