model-checker : verification of current_heap

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 9907998..e7a8de6 100644 (file)
--- 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 678d417..5191222 100644 (file)
--- 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;
     
 }