model-checker : fix some memory leaks

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index e3bec58..f04ea98 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -27,7 +27,7 @@ int create_dump(int pair)
   switch(fork()){
   case 0:
     // We are the child process -- run the actual program
-    abort();
+    xbt_abort();
     break;
     
   case -1:
@@ -83,9 +83,7 @@ int reached(xbt_state_t st){
     /* New pair reached */
     xbt_dynar_push(reached_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
-    
-    create_dump(xbt_dynar_length(reached_pairs));
-
+ 
     return 0;
 
   }else{
@@ -116,8 +114,6 @@ int reached(xbt_state_t st){
       }
     }
 
-    create_dump(xbt_dynar_length(reached_pairs));
-
     /* New pair reached */
     xbt_dynar_push(reached_pairs, &new_pair); 
     
@@ -166,8 +162,6 @@ void set_pair_reached(xbt_state_t st){
   
   MC_UNSET_RAW_MEM;
 
-  create_dump(xbt_dynar_length(reached_pairs));
-
   if(raw_mem_set)
     MC_SET_RAW_MEM;
   else
@@ -223,12 +217,14 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 
 /********************* Double-DFS stateless *******************/
 
-void MC_pair_stateless_delete(mc_pair_stateless_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
+void pair_stateless_free(mc_pair_stateless_t pair){
   xbt_free(pair);
 }
 
+void pair_stateless_free_voidp(void *p){
+  pair_stateless_free((mc_pair_stateless_t) * (void **) p);
+}
+
 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   mc_pair_stateless_t p = NULL;
   p = xbt_new0(s_mc_pair_stateless_t, 1);
@@ -239,6 +235,19 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   return p;
 }
 
+void pair_reached_free(mc_pair_reached_t pair){
+  if(pair){
+    pair->automaton_state = NULL;
+    xbt_dynar_free(&(pair->prop_ato));
+    MC_free_snapshot(pair->system_state);
+    xbt_free(pair);
+  }
+}
+
+void pair_reached_free_voidp(void *p){
+  pair_reached_free((mc_pair_reached_t) * (void **) p);
+}
+
 void MC_ddfs_init(void){
 
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -263,7 +272,7 @@ void MC_ddfs_init(void){
     }
   }
 
-  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
+  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 
   /* Save the initial state */
@@ -272,6 +281,10 @@ void MC_ddfs_init(void){
 
   MC_UNSET_RAW_MEM; 
 
+  /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
+  get_libsimgrid_plt_section();
+  get_binary_plt_section();
+
   unsigned int cursor = 0;
   xbt_state_t state;