model-checker : init MC for liveness in a separate function

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index b6721f6..984323b 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -112,6 +112,41 @@ void MC_take_snapshot(mc_snapshot_t snapshot)
   free_memory_map(maps);
 }
 
   free_memory_map(maps);
 }
 

+void MC_init_memory_map_info(){
+  
+  unsigned int i = 0;
+  s_map_region_t reg;
+  memory_map_t maps = get_memory_map();
+
+   while (i < maps->mapsize) {
+    reg = maps->regions[i];
+    if ((reg.prot & PROT_WRITE)){
+      if (maps->regions[i].pathname == NULL){
+        if(reg.start_addr == raw_heap){
+          end_raw_heap = reg.end_addr;
+        }
+      } else {
+        if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
+          start_data_libsimgrid = reg.start_addr;
+        }
+      }
+    }else if ((reg.prot & PROT_READ)){
+      if (maps->regions[i].pathname != NULL){
+        if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
+          start_text_libsimgrid = reg.start_addr;
+          libsimgrid_path = strdup(maps->regions[i].pathname);
+        }else{
+          if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
+            start_text_binary = reg.start_addr;
+          }
+        }
+      }
+    }
+    i++;
+  }
+
+}
+

 mc_snapshot_t MC_take_snapshot_liveness()
 {
 
 mc_snapshot_t MC_take_snapshot_liveness()
 {
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 8bb0aa6..9c56d81 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -146,7 +146,6 @@ void MC_init_safety(void)
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 

-

   if(raw_mem_set)
     MC_SET_RAW_MEM;
   else
   if(raw_mem_set)
     MC_SET_RAW_MEM;
   else


@@ -166,12 +165,7 @@ void MC_modelcheck(void)
   MC_exit();
 }
 
   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);
 
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 


@@ -198,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);
   /* 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);
   
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 9dd5b58..8d58c64 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -245,6 +245,8 @@ void MC_exit_liveness(void);
 mc_state_t MC_state_pair_new(void);
 void pair_reached_free(mc_pair_reached_t pair);
 void pair_reached_free_voidp(void *p);
 mc_state_t MC_state_pair_new(void);
 void pair_reached_free(mc_pair_reached_t pair);
 void pair_reached_free_voidp(void *p);

+void MC_init_liveness(void);
+void MC_init_memory_map_info(void);

 
 /* **** Double-DFS stateless **** */
 
 
 /* **** Double-DFS stateless **** */