model-checker : verification of current_heap

[simgrid.git] / src / mc / mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index d4cbfe6..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;
     
 }
 
@@ -274,7 +273,8 @@ void MC_ddfs_init(void){
   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 
   /* Save the initial state */
-  initial_snapshot_liveness = MC_take_snapshot_liveness();
+  initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+  initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
 
   MC_UNSET_RAW_MEM; 
   
@@ -290,7 +290,7 @@ void MC_ddfs_init(void){
       MC_UNSET_RAW_MEM;
       
       if(cursor != 0){
-        MC_restore_snapshot(initial_snapshot_liveness);
+        MC_restore_snapshot(initial_state_liveness->initial_snapshot);
         MC_UNSET_RAW_MEM;
       }
 
@@ -307,7 +307,7 @@ void MC_ddfs_init(void){
         set_pair_reached(state);
 
         if(cursor != 0){
-          MC_restore_snapshot(initial_snapshot_liveness);
+          MC_restore_snapshot(initial_state_liveness->initial_snapshot);
           MC_UNSET_RAW_MEM;
         }