model-checker : remove binary name as argument of some functions, available with...

diff --git a/examples/msg/mc/bugged1_for_liveness.c b/examples/msg/mc/bugged1_for_liveness.c
index b45f9ce..7ca139c 100644 (file)
--- a/examples/msg/mc/bugged1_for_liveness.c
+++ b/examples/msg/mc/bugged1_for_liveness.c
@@ -141,7 +141,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_bugged1_liveness.xml");
-  MSG_main_liveness(automaton, argv[0]);
+  MSG_main_liveness(automaton);
 
   return 0;
 }

diff --git a/examples/msg/mc/bugged1_while_liveness.c b/examples/msg/mc/bugged1_while_liveness.c
index bc14d0b..1e56dad 100644 (file)
--- a/examples/msg/mc/bugged1_while_liveness.c
+++ b/examples/msg/mc/bugged1_while_liveness.c
@@ -131,7 +131,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_bugged1_liveness.xml");
-  MSG_main_liveness(automaton, argv[0]);
+  MSG_main_liveness(automaton);
 
   return 0;
 }

diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 15467be..8a060a3 100644 (file)
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -188,7 +188,7 @@ int main(int argc, char *argv[])
   MSG_function_register("consumer", consumer);
   MSG_function_register("producer", producer);
   MSG_launch_application("deploy_bugged2_liveness.xml");
-  MSG_main_liveness(automaton, argv[0]);
+  MSG_main_liveness(automaton);
 
   return 0;
 

diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c
index 54804fa..77183df 100644 (file)
--- a/examples/msg/mc/centralized_liveness.c
+++ b/examples/msg/mc/centralized_liveness.c
@@ -110,7 +110,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_liveness.xml");
-  MSG_main_liveness(automaton, argv[0]);
+  MSG_main_liveness(automaton);
 
   return 0;
 

diff --git a/examples/msg/mc/centralized_liveness_deadlock.c b/examples/msg/mc/centralized_liveness_deadlock.c
index 5f58118..ba050d6 100644 (file)
--- a/examples/msg/mc/centralized_liveness_deadlock.c
+++ b/examples/msg/mc/centralized_liveness_deadlock.c
@@ -107,7 +107,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_liveness.xml");
-  MSG_main_liveness(automaton, argv[0]);
+  MSG_main_liveness(automaton);
 
   return 0;
 

diff --git a/examples/msg/mc/test_snapshot.c b/examples/msg/mc/test_snapshot.c
index fad4288..865ece3 100644 (file)
--- a/examples/msg/mc/test_snapshot.c
+++ b/examples/msg/mc/test_snapshot.c
@@ -141,7 +141,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_test_snapshot.xml");
-  MSG_main_liveness(automaton, argv[0]);
+  MSG_main_liveness(automaton);
 
   return 0;
 }

diff --git a/include/msg/msg.h b/include/msg/msg.h
index c9c5449..b69b691 100644 (file)
--- a/include/msg/msg.h
+++ b/include/msg/msg.h
@@ -39,7 +39,7 @@ XBT_PUBLIC(void) MSG_global_init(int *argc, char **argv);
 XBT_PUBLIC(void) MSG_global_init_args(int *argc, char **argv);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
 XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);
-XBT_PUBLIC(MSG_error_t) MSG_main_liveness(xbt_automaton_t a, char *prgm);
+XBT_PUBLIC(MSG_error_t) MSG_main_liveness(xbt_automaton_t a);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
                                        xbt_main_func_t code);

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 1fe6b57..3073498 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -25,7 +25,7 @@ XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
 XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(void) MC_modelcheck_stateful(void);
-XBT_PUBLIC(void) MC_modelcheck_liveness(xbt_automaton_t a, char *prgm);
+XBT_PUBLIC(void) MC_modelcheck_liveness(xbt_automaton_t a);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
 

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 2fbb5be..f130c0b 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -5,6 +5,7 @@
 
 #include <libgen.h>
 #include "mc_private.h"
+#include <xbt/module.h>
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
@@ -139,7 +140,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
         if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
           MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
         } else {
-         if (!memcmp(basename(maps->regions[i].pathname), basename(prog_name), strlen(basename(prog_name)))){
+         if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
            MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
          } 
        }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index c0b7acd..e9e5940 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -37,9 +37,8 @@ xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 
 xbt_automaton_t automaton;
-char *prog_name;
 
-static void MC_init_liveness(xbt_automaton_t a, char *prgm);
+static void MC_init_liveness(xbt_automaton_t a);
 static void MC_assert_pair(int prop);
 
 
@@ -104,7 +103,7 @@ void MC_init_safety_stateful(void){
 
 }
 
-static void MC_init_liveness(xbt_automaton_t a, char *prgm){
+static void MC_init_liveness(xbt_automaton_t a){
 
   XBT_DEBUG("Start init mc");
   
@@ -126,7 +125,6 @@ static void MC_init_liveness(xbt_automaton_t a, char *prgm){
   MC_UNSET_RAW_MEM;
 
   automaton = a;
-  prog_name = strdup(prgm);
 
   MC_ddfs_init();
 
@@ -149,8 +147,8 @@ void MC_modelcheck_stateful(void)
 }
 
 
-void MC_modelcheck_liveness(xbt_automaton_t a, char *prgm){
-  MC_init_liveness(a, prgm);
+void MC_modelcheck_liveness(xbt_automaton_t a){
+  MC_init_liveness(a);
   MC_exit_liveness();
 }
 

diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index d1a8e5a..555f8aa 100644 (file)
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -141,14 +141,14 @@ MSG_error_t MSG_main_stateful(void)
 }
 
 
-MSG_error_t MSG_main_liveness(xbt_automaton_t a, char *prgm)
+MSG_error_t MSG_main_liveness(xbt_automaton_t a)
 {
   /* Clean IO before the run */
   fflush(stdout);
   fflush(stderr);
 
   if (MC_IS_ENABLED) {
-    MC_modelcheck_liveness(a, prgm);
+    MC_modelcheck_liveness(a);
   }
   else {
     SIMIX_run();