model-checker : store initial snapshot in structure malloced in raw_heap

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 28a5c4e..bab8f71 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -73,7 +73,7 @@ mc_stats_t mc_stats = NULL;
 
 mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
-mc_snapshot_t initial_snapshot_liveness = NULL;
+mc_global_t initial_state_liveness = NULL;
 int compare;
 
 /* Local */
@@ -371,9 +371,10 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Restore the initial state */
-  MC_restore_snapshot(initial_snapshot_liveness);
+  MC_restore_snapshot(initial_state_liveness->initial_snapshot);
   /* At the moment of taking the snapshot the raw heap was set, so restoring
    * it will set it back again, we have to unset it to continue  */
+  
   MC_UNSET_RAW_MEM;
 
   if(all_stack){

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index d4cbfe6..678d417 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -274,7 +274,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 +291,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 +308,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;
         }
   

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 8d58c64..808f36c 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -42,6 +42,10 @@ typedef struct s_mc_snapshot_stack{
   void *stack_pointer;
 }s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
 
+typedef struct s_mc_global_t{
+  mc_snapshot_t initial_snapshot;
+}s_mc_global_t, *mc_global_t;
+
 void MC_take_snapshot(mc_snapshot_t);
 mc_snapshot_t MC_take_snapshot_liveness(void);
 void MC_restore_snapshot(mc_snapshot_t);
@@ -213,7 +217,7 @@ void MC_init_safety(void);
 /********************************** Double-DFS for liveness property**************************************/
 
 extern xbt_fifo_t mc_stack_liveness;
-extern mc_snapshot_t initial_snapshot_liveness;
+extern mc_global_t initial_state_liveness;
 extern xbt_automaton_t _mc_property_automaton;
 extern int compare;
 extern void *start_plt_libsimgrid;