From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Thu, 18 Oct 2012 19:22:20 +0000 (+0200)
Subject: model-checker : change MC_take_snapshot_liveness declaration (snapshot returned inste... 
X-Git-Tag: v3_9_rc1~91^2~179
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0caa7c0ef3bfec3dc4b7dfb265c5570f46346782

model-checker : change MC_take_snapshot_liveness declaration (snapshot returned instead of in parameters) and check heap used
---

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 47d1be9239..ad1de431dc 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -112,9 +112,15 @@ void MC_take_snapshot(mc_snapshot_t snapshot)
   free_memory_map(maps);
 }
 
-void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
+mc_snapshot_t MC_take_snapshot_liveness()
 {
 
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
+  mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
+
   unsigned int i = 0;
   s_map_region_t reg;
   memory_map_t maps = get_memory_map();
@@ -176,6 +182,13 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
   
   free_memory_map(maps);
 
+  MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+
+  return snapshot;
+
 }
 
 void MC_restore_snapshot(mc_snapshot_t snapshot)
diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 1510ccaff8..b91d4e431b 100644
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -140,6 +140,10 @@ void heap_equality_free_voidp(void *e){
 
 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  
+  MC_SET_RAW_MEM;
+
   int errors = 0, i;
   xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
   xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
@@ -167,6 +171,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
@@ -174,6 +180,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){
@@ -181,6 +189,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;  
         return 1; 
       }
       heap1 = s1->regions[i]->data;
@@ -193,6 +203,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
@@ -200,6 +212,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
@@ -207,6 +221,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       break;
@@ -218,6 +234,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
@@ -225,6 +243,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
@@ -232,6 +252,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }
       break;
@@ -261,6 +283,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_dynar_free(&stacks1);
         xbt_dynar_free(&stacks2);
         xbt_dynar_free(&equals);
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
         return 1;
       }else{
         XBT_INFO("Local variables are equals in stack %d", cursor + 1);
@@ -274,6 +298,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   xbt_dynar_free(&stacks1);
   xbt_dynar_free(&stacks2);
   xbt_dynar_free(&equals);
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
   return 0;
   
 }
diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index b7d7681cf1..1fb8fbfd04 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -61,8 +61,7 @@ int reached(xbt_state_t st){
   new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1); 
-  MC_take_snapshot_liveness(new_pair->system_state);  
+  new_pair->system_state = MC_take_snapshot_liveness();  
   
   /* Get values of propositional symbols */
   int res;
@@ -143,8 +142,7 @@ void set_pair_reached(xbt_state_t st){
   pair->nb = xbt_dynar_length(reached_pairs) + 1;
   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->system_state = xbt_new0(s_mc_snapshot_t, 1); 
-  MC_take_snapshot_liveness(pair->system_state);
+  pair->system_state = MC_take_snapshot_liveness();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;
@@ -276,15 +274,10 @@ void MC_ddfs_init(void){
   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 
   /* Save the initial state */
-  initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(initial_snapshot_liveness);
+  initial_snapshot_liveness = MC_take_snapshot_liveness();
 
   MC_UNSET_RAW_MEM; 
-
-  /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
-  get_libsimgrid_plt_section();
-  get_binary_plt_section();
-
+  
   unsigned int cursor = 0;
   xbt_state_t state;
 
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 9c0f06516c..9dd5b58df3 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -43,7 +43,7 @@ typedef struct s_mc_snapshot_stack{
 }s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
 
 void MC_take_snapshot(mc_snapshot_t);
-void MC_take_snapshot_liveness(mc_snapshot_t s);
+mc_snapshot_t MC_take_snapshot_liveness(void);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 void snapshot_stack_free_voidp(void *s);