user_main: pass remaining arguments to the user program

diff --git a/libthreads.h b/libthreads.h
index 0c02971342d06ffa903feb01b2d4daadc08754d4..8033a12dc053fe02a223b158934722331da96e8d 100644 (file)
--- a/libthreads.h
+++ b/libthreads.h
@@ -18,7 +18,7 @@ extern "C" {
        int thrd_yield(void);
        thrd_t thrd_current(void);
 
        int thrd_yield(void);
        thrd_t thrd_current(void);
 

-       void user_main(void);
+       int user_main(int, char**);

 
 #ifdef __cplusplus
 }
 
 #ifdef __cplusplus
 }

diff --git a/main.cc b/main.cc
index 853654ccd35626c8410842f15419b265accd2dbb..2a4119a6acb940e615f1342eb715732c13427357 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;
 
 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;
 /** 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 */
        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();
 
                /* Wait for all threads to complete */
                model->finish_execution();

diff --git a/test/double-relseq.c b/test/double-relseq.c
index 5b220eb888c08f81610516d82c7d44f884054cec..369265a7d6246eb3a250ac1297821d53189ecf7f 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);
 }
 
        atomic_store_explicit(&x, 2, memory_order_relaxed);
 }
 

-void user_main()
+int user_main(int argc, char **argv)

 {
        thrd_t t1, t2, t3, t4;
 
 {
        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());
        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 896ae30b2dd54cd97f4e18fda4de60face50e018..a14ed02028796a422cd4f6ae7b20d8323796e093 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);
 {
        thrd_t t1, t2;
        atomic_init(&mylock.lock, RW_LOCK_BIAS);


@@ -107,4 +107,6 @@ void user_main()
 
        thrd_join(t1);
        thrd_join(t2);
 
        thrd_join(t1);
        thrd_join(t2);

+
+       return 0;

 }
 }

diff --git a/test/pending-release.c b/test/pending-release.c
index f3ae9f43420b2cdc5de5e8cf59cf4c72921ecba9..739c45e0f675931507e35e9b656a767fdf04fb5d 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);
 }
 
        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;
 {
        thrd_t t1, t2, t5;
        int i = 4;


@@ -60,4 +60,6 @@ void user_main()
        thrd_join(t1);
        thrd_join(t2);
        thrd_join(t5);
        thrd_join(t1);
        thrd_join(t2);
        thrd_join(t5);

+
+       return 0;

 }
 }

diff --git a/test/releaseseq.c b/test/releaseseq.c
index 462a59f32a30251de82bed4ffbe451b8b862ed0b..27f2fb1cb8e5f5a357ce3da6a981f5e223538281 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);
 }
 
        atomic_store_explicit(&x, 2, memory_order_relaxed);
 }
 

-void user_main()
+int user_main(int argc, char **argv)

 {
        thrd_t t1, t2, t3;
 
 {
        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());
        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 c3a5ea82fb328b793b967707b2a2c3ec2cb38990..a74ae426ca95df7e90f63424d4aaaa3a327e7292 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);
 }
 
        atomic_fetch_add_explicit(&x, 1, memory_order_relaxed);
 }
 

-void user_main()
+int user_main(int argc, char **argv)

 {
        thrd_t t1, t2;
 
 {
        thrd_t t1, t2;
 


@@ -22,4 +22,6 @@ void user_main()
 
        thrd_join(t1);
        thrd_join(t2);
 
        thrd_join(t1);
        thrd_join(t2);

+
+       return 0;

 }
 }

diff --git a/test/userprog.c b/test/userprog.c
index 645dc3095a366abeb79c976d6d456b6381760a17..b45e8f9dcebe338cfa4374a75c8aaaa45e54a92b 100644 (file)
--- a/test/userprog.c
+++ b/test/userprog.c
@@ -21,7 +21,7 @@ static void b(void *obj)
        printf("r2=%u\n",r2);
 }
 
        printf("r2=%u\n",r2);
 }
 

-void user_main()
+int user_main(int argc, char **argv)

 {
        thrd_t t1, t2;
 
 {
        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());
        thrd_join(t1);
        thrd_join(t2);
        printf("Thread %d is finished\n", thrd_current());

+
+       return 0;

 }
 }