From 324ed35d0489e7df64745a022a3d426ff227fba2 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 13 Jun 2012 11:19:24 +0200 Subject: [PATCH] model-checker : remove binary name as argument of some functions, available with xbt_binary_name --- examples/msg/mc/bugged1_for_liveness.c | 2 +- examples/msg/mc/bugged1_while_liveness.c | 2 +- examples/msg/mc/bugged2_liveness.c | 2 +- examples/msg/mc/centralized_liveness.c | 2 +- examples/msg/mc/centralized_liveness_deadlock.c | 2 +- examples/msg/mc/test_snapshot.c | 2 +- include/msg/msg.h | 2 +- src/include/mc/mc.h | 2 +- src/mc/mc_checkpoint.c | 3 ++- src/mc/mc_global.c | 10 ++++------ src/msg/msg_global.c | 4 ++-- 11 files changed, 16 insertions(+), 17 deletions(-) diff --git a/examples/msg/mc/bugged1_for_liveness.c b/examples/msg/mc/bugged1_for_liveness.c index b45f9ceafd..7ca139c95e 100644 --- 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 bc14d0b915..1e56dada33 100644 --- 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 15467bee43..8a060a3f32 100644 --- 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 54804faf2f..77183df608 100644 --- 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 5f58118744..ba050d64c3 100644 --- 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 fad42885c5..865ece3cba 100644 --- 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 c9c5449410..b69b69163f 100644 --- 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 1fe6b57339..3073498062 100644 --- 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 2fbb5bef62..f130c0b6c6 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -5,6 +5,7 @@ #include #include "mc_private.h" +#include 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 c0b7acddda..e9e5940b46 100644 --- 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 d1a8e5a0bd..555f8aae93 100644 --- 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(); -- 2.30.2