From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 31 Oct 2012 17:47:48 +0000 (+0100)
Subject: model-checker : verification of current_heap
X-Git-Tag: v3_9_rc1~91^2~126^2~26
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0645cbd02f4f44ea8d916a2093c1776002ebdcf4

model-checker : verification of current_heap
---

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 990799806c..e7a8de6b3f 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -292,7 +292,7 @@ int MC_deadlock_check()
  */
 void MC_replay(xbt_fifo_t stack, int start)
 {
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 
   int value, i = 1;
   char *req_str;
@@ -348,7 +348,7 @@ void MC_replay(xbt_fifo_t stack, int start)
   }
   XBT_DEBUG("**** End Replay ****");
 
-  if(raw_mem_set)
+  if(raw_mem)
     MC_SET_RAW_MEM;
   else
     MC_UNSET_RAW_MEM;
@@ -359,7 +359,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 {
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 
   int value;
   char *req_str;
@@ -462,7 +462,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
   XBT_DEBUG("**** End Replay ****");
 
-  if(raw_mem_set)
+  if(raw_mem)
     MC_SET_RAW_MEM;
   else
     MC_UNSET_RAW_MEM;
diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 678d417188..51912227c6 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -82,6 +82,9 @@ int reached(xbt_state_t st){
     /* New pair reached */
     xbt_dynar_push(reached_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
+
+    if(raw_mem_set)
+      MC_SET_RAW_MEM;
  
     return 0;
 
@@ -120,9 +123,7 @@ int reached(xbt_state_t st){
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
-    else
-      MC_UNSET_RAW_MEM;
-
+ 
     compare = 0;
     
     return 0;
@@ -162,8 +163,6 @@ void set_pair_reached(xbt_state_t st){
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
     
 }