user_main: pass remaining arguments to the user program

diff --git a/libthreads.h b/libthreads.h
index 0c02971..8033a12 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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;
 }