model-checker : free memory at the end of stateless double-dfs algorithm

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 35e5156..c693825 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -11,6 +11,7 @@ extern mc_snapshot_t initial_snapshot;
 
 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
+  XBT_DEBUG("Compare snapshot");
   
   if(s1->num_reg != s2->num_reg){
     XBT_DEBUG("Different num_reg");
@@ -210,8 +211,6 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   return p;
 }
 
-
-
 void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
 
   XBT_DEBUG("**************************************************");
@@ -605,9 +604,14 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
   xbt_fifo_shift(mc_stack_liveness_stateless);
   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
     xbt_fifo_shift(reached_pairs);
-    MC_free_snapshot(snapshot);
   }
+  if(snapshot != NULL)
+    MC_free_snapshot(snapshot);
   MC_UNSET_RAW_MEM;
 
+  MC_pair_stateless_delete(current_pair);
+
+  /* FIXME : free memory (pair, snapshot)*/
+
 }