X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0b892a9de2e4218184dc0b0726773f386bb38b65..0275d08cbb6554fc92eff095847ea32f049e37e9:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 421479dbd6..9c56d814d7 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -23,6 +23,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
 /* Configuration support */
 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
 
+
 extern int _surf_init_status;
 void _mc_cfg_cb_reduce(const char *name, int pos) {
   if (_surf_init_status && !_surf_do_model_check) {
@@ -145,7 +146,6 @@ void MC_init_safety(void)
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 
-
   if(raw_mem_set)
     MC_SET_RAW_MEM;
   else
@@ -165,12 +165,7 @@ void MC_modelcheck(void)
   MC_exit();
 }
 
-void MC_modelcheck_liveness(){
-
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  /* init stuff */
-  XBT_INFO("Start init mc");
+void MC_init_liveness(){
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
@@ -197,6 +192,24 @@ void MC_modelcheck_liveness(){
   /* Get local variables in libsimgrid for state equality detection */
   xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path);
   MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables);
+
+  MC_UNSET_RAW_MEM;
+
+  MC_init_memory_map_info();
+
+  /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
+  get_libsimgrid_plt_section();
+  get_binary_plt_section();
+
+}
+
+void MC_modelcheck_liveness(){
+
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_init_liveness();
+ 
+  MC_SET_RAW_MEM;
   
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
@@ -549,7 +562,7 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
   MC_SET_RAW_MEM;
   while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
-    MC_pair_stateless_delete(pair);
+    pair_stateless_free(pair);
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
@@ -585,7 +598,7 @@ void MC_print_statistics_pairs(mc_stats_pair_t stats)
 
 void MC_assert(int prop)
 {
-  if (MC_IS_ENABLED && !prop){
+  if (MC_is_active() && !prop){
     XBT_INFO("**************************");
     XBT_INFO("*** PROPERTY NOT VALID ***");
     XBT_INFO("**************************");
@@ -597,7 +610,7 @@ void MC_assert(int prop)
 }
 
 static void MC_assert_pair(int prop){
-  if (MC_IS_ENABLED && !prop) {
+  if (MC_is_active() && !prop) {
     XBT_INFO("**************************");
     XBT_INFO("*** PROPERTY NOT VALID ***");
     XBT_INFO("**************************");
@@ -702,16 +715,18 @@ void MC_ignore(void *address, size_t size){
 
 void MC_new_stack_area(void *stack, char *name, void* context){
 
+  MC_SET_RAW_MEM;
+
   if(stacks_areas == NULL)
     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-
-  MC_SET_RAW_MEM;
+  
   stack_region_t region = NULL;
   region = xbt_new0(s_stack_region_t, 1);
   region->address = stack;
   region->process_name = strdup(name);
   region->context = context;
   xbt_dynar_push(stacks_areas, &region);
+  
   MC_UNSET_RAW_MEM;
 }