From: Brian Norris <banorris@uci.edu>
Date: Tue, 9 Oct 2012 01:36:06 +0000 (-0700)
Subject: user_main: pass remaining arguments to the user program
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=b59d5f84ac4800cc144fc7c8837d96181423d9ae;p=cdsspec-compiler.git

user_main: pass remaining arguments to the user program
---

diff --git a/libthreads.h b/libthreads.h
index 0c02971..8033a12 100644
--- a/libthreads.h
+++ b/libthreads.h
@@ -18,7 +18,7 @@ extern "C" {
 	int thrd_yield(void);
 	thrd_t thrd_current(void);
 
-	void user_main(void);
+	int user_main(int, char**);
 
 #ifdef __cplusplus
 }
diff --git a/main.cc b/main.cc
index 853654c..2a4119a 100644
--- a/main.cc
+++ b/main.cc
@@ -77,6 +77,12 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
 int main_argc;
 char **main_argv;
 
+/** Wrapper to run the user's main function, with appropriate arguments */
+void wrapper_user_main(void *)
+{
+	user_main(main_argc, main_argv);
+}
+
 /** The model_main function contains the main model checking loop. */
 static void model_main() {
 	thrd_t user_thread;
@@ -97,7 +103,7 @@ static void model_main() {
 	snapshotObject->snapshotStep(0);
 	do {
 		/* Start user program */
-		model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
+		model->add_thread(new Thread(&user_thread, &wrapper_user_main, NULL));
 
 		/* Wait for all threads to complete */
 		model->finish_execution();
diff --git a/test/double-relseq.c b/test/double-relseq.c
index 5b220eb..369265a 100644
--- a/test/double-relseq.c
+++ b/test/double-relseq.c
@@ -37,7 +37,7 @@ static void c(void *obj)
 	atomic_store_explicit(&x, 2, memory_order_relaxed);
 }
 
-void user_main()
+int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2, t3, t4;
 
@@ -54,4 +54,6 @@ void user_main()
 	thrd_join(t3);
 	thrd_join(t4);
 	printf("Thread %d is finished\n", thrd_current());
+
+	return 0;
 }
diff --git a/test/linuxrwlocks.c b/test/linuxrwlocks.c
index 896ae30..a14ed02 100644
--- a/test/linuxrwlocks.c
+++ b/test/linuxrwlocks.c
@@ -97,7 +97,7 @@ static void a(void *obj)
 	}
 }
 
-void user_main()
+int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2;
 	atomic_init(&mylock.lock, RW_LOCK_BIAS);
@@ -107,4 +107,6 @@ void user_main()
 
 	thrd_join(t1);
 	thrd_join(t2);
+
+	return 0;
 }
diff --git a/test/pending-release.c b/test/pending-release.c
index f3ae9f4..739c45e 100644
--- a/test/pending-release.c
+++ b/test/pending-release.c
@@ -46,7 +46,7 @@ static void c(void *obj)
 	atomic_store_explicit(&x, 22, memory_order_relaxed);
 }
 
-void user_main()
+int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2, t5;
 	int i = 4;
@@ -60,4 +60,6 @@ void user_main()
 	thrd_join(t1);
 	thrd_join(t2);
 	thrd_join(t5);
+
+	return 0;
 }
diff --git a/test/releaseseq.c b/test/releaseseq.c
index 462a59f..27f2fb1 100644
--- a/test/releaseseq.c
+++ b/test/releaseseq.c
@@ -32,7 +32,7 @@ static void c(void *obj)
 	atomic_store_explicit(&x, 2, memory_order_relaxed);
 }
 
-void user_main()
+int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2, t3;
 
@@ -47,4 +47,6 @@ void user_main()
 	thrd_join(t2);
 	thrd_join(t3);
 	printf("Thread %d is finished\n", thrd_current());
+
+	return 0;
 }
diff --git a/test/rmwprog.c b/test/rmwprog.c
index c3a5ea8..a74ae42 100644
--- a/test/rmwprog.c
+++ b/test/rmwprog.c
@@ -12,7 +12,7 @@ static void a(void *obj)
 	atomic_fetch_add_explicit(&x, 1, memory_order_relaxed);
 }
 
-void user_main()
+int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2;
 
@@ -22,4 +22,6 @@ void user_main()
 
 	thrd_join(t1);
 	thrd_join(t2);
+
+	return 0;
 }
diff --git a/test/userprog.c b/test/userprog.c
index 645dc30..b45e8f9 100644
--- a/test/userprog.c
+++ b/test/userprog.c
@@ -21,7 +21,7 @@ static void b(void *obj)
 	printf("r2=%u\n",r2);
 }
 
-void user_main()
+int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2;
 
@@ -35,4 +35,6 @@ void user_main()
 	thrd_join(t1);
 	thrd_join(t2);
 	printf("Thread %d is finished\n", thrd_current());
+
+	return 0;
 }