model-checker : fix some memory leaks

diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h
index 49df463..9f57747 100644 (file)
--- a/include/xbt/automaton.h
+++ b/include/xbt/automaton.h
@@ -60,6 +60,7 @@ typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t;
 
 
 XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);
 
 
 XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);

+

 XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);
 XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);


@@ -74,12 +75,6 @@ XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a);
 
 XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst);
 
 
 XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst);
 

-XBT_PUBLIC(void) xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function);
-
-XBT_PUBLIC(void) xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function);
-
-XBT_PUBLIC(void) xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function);
-

 XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t);
 XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t);


@@ -110,6 +105,17 @@ XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
 
 XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2);
 
 
 XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2);
 

+XBT_PUBLIC(void) xbt_state_free_voidp(void *s);
+
+XBT_PUBLIC(void) xbt_state_free(xbt_state_t s);
+
+XBT_PUBLIC(void) xbt_transition_free_voidp(void *t);
+
+XBT_PUBLIC(void) xbt_exp_label_free_voidp(void *e);
+
+XBT_PUBLIC(void) xbt_propositional_symbol_free_voidp(void *ps);
+
+XBT_PUBLIC(void) xbt_automaton_free(xbt_automaton_t a);

 
 SG_END_DECL()
 
 
 SG_END_DECL()
 

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index a31625a..61cef5d 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -37,5 +37,8 @@ typedef struct s_heap_equality{
   void *address2;
 }s_heap_equality_t, *heap_equality_t;
 
   void *address2;
 }s_heap_equality_t, *heap_equality_t;
 

+void heap_equality_free_voidp(void *e);
+void stack_region_free_voidp(void *s);
+

 SG_END_DECL()
 #endif                          /* _MC_MC_H */
 SG_END_DECL()
 #endif                          /* _MC_MC_H */

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 8a5861c..5384c38 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -34,6 +34,8 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
 static void print_local_variables_values(xbt_dynar_t all_variables);
 static void *get_stack_pointer(void *stack_context, void *heap);
 
 static void print_local_variables_values(xbt_dynar_t all_variables);
 static void *get_stack_pointer(void *stack_context, void *heap);
 

+static void snapshot_stack_free(mc_snapshot_stack_t s);
+

 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size)
 {
   mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1);
 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size)
 {
   mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1);


@@ -191,6 +193,7 @@ void MC_free_snapshot(mc_snapshot_t snapshot)
   for(i=0; i < snapshot->num_reg; i++)
     MC_region_destroy(snapshot->regions[i]);
 
   for(i=0; i < snapshot->num_reg; i++)
     MC_region_destroy(snapshot->regions[i]);
 

+  xbt_dynar_free(&(snapshot->stacks));

   xbt_free(snapshot);
 }
 
   xbt_free(snapshot);
 }
 


@@ -545,3 +548,15 @@ static void print_local_variables_values(xbt_dynar_t all_variables){
   }
 }
 
   }
 }
 

+
+static void snapshot_stack_free(mc_snapshot_stack_t s){
+  if(s){
+    xbt_free(s->local_variables->data);
+    xbt_free(s->local_variables);
+    xbt_free(s);
+  }
+}
+
+void snapshot_stack_free_voidp(void *s){
+  snapshot_stack_free((mc_snapshot_stack_t) * (void **) s);
+}

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 503d498..1510cca 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -18,6 +18,9 @@ static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *
 static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
 static size_t ignore(void *address);
 
 static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
 static size_t ignore(void *address);
 

+static void stack_region_free(stack_region_t s);
+static void heap_equality_free(heap_equality_t e);
+

 static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals);
 
 static size_t ignore(void *address){
 static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals);
 
 static size_t ignore(void *address){


@@ -114,12 +117,33 @@ static int heap_region_compare(void *d1, void *d2, size_t size){
   return distance;
 }
 
   return distance;
 }
 

+static void stack_region_free(stack_region_t s){
+  if(s){
+    xbt_free(s->process_name);
+    xbt_free(s);
+  }
+}
+
+void stack_region_free_voidp(void *s){
+  stack_region_free((stack_region_t) * (void **) s);
+}
+
+static void heap_equality_free(heap_equality_t e){
+  if(e){
+    xbt_free(e);
+  }
+}
+
+void heap_equality_free_voidp(void *e){
+  heap_equality_free((heap_equality_t) * (void **) e);
+}
+

 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   int errors = 0, i;
 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   int errors = 0, i;

-  xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), NULL);
-  xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), NULL);
-  xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), NULL);
+  xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
+  xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
+  xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);

 
   void *heap1 = NULL, *heap2 = NULL;
   
 
   void *heap1 = NULL, *heap2 = NULL;
   


@@ -140,14 +164,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       /* Compare heapregion */
       if(s1->regions[i]->size != s2->regions[i]->size){
         XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
       /* Compare heapregion */
       if(s1->regions[i]->size != s2->regions[i]->size){
         XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
         XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
         XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){
         XBT_INFO("Different heap (mmalloc_compare)");
         return 1;
       }
       if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){
         XBT_INFO("Different heap (mmalloc_compare)");

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1; 
       }
       heap1 = s1->regions[i]->data;
         return 1; 
       }
       heap1 = s1->regions[i]->data;


@@ -157,14 +190,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       /* Compare data libsimgrid region */
       if(s1->regions[i]->size != s2->regions[i]->size){
         XBT_INFO("Different size of libsimgrid (data) (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
       /* Compare data libsimgrid region */
       if(s1->regions[i]->size != s2->regions[i]->size){
         XBT_INFO("Different size of libsimgrid (data) (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
         XBT_INFO("Different start addr of libsimgrid (data) (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
         XBT_INFO("Different start addr of libsimgrid (data) (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
         XBT_INFO("Different memcmp for data in libsimgrid");
         return 1;
       }
       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
         XBT_INFO("Different memcmp for data in libsimgrid");

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       break;
         return 1;
       }
       break;


@@ -173,14 +215,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       /* Compare data program region */
       if(s1->regions[i]->size != s2->regions[i]->size){
         XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
       /* Compare data program region */
       if(s1->regions[i]->size != s2->regions[i]->size){
         XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
         XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
         return 1;
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
         XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
         XBT_INFO("Different memcmp for data in program");
         return 1;
       }
       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
         XBT_INFO("Different memcmp for data in program");

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }
       break;
         return 1;
       }
       break;


@@ -207,6 +258,9 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals);
       if(diff_local > 0){
         XBT_INFO("Hamming distance between stacks : %d", diff);
       diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals);
       if(diff_local > 0){
         XBT_INFO("Hamming distance between stacks : %d", diff);

+        xbt_dynar_free(&stacks1);
+        xbt_dynar_free(&stacks2);
+        xbt_dynar_free(&equals);

         return 1;
       }else{
         XBT_INFO("Local variables are equals in stack %d", cursor + 1);
         return 1;
       }else{
         XBT_INFO("Local variables are equals in stack %d", cursor + 1);


@@ -217,6 +271,9 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     cursor++;
   }
 
     cursor++;
   }
 

+  xbt_dynar_free(&stacks1);
+  xbt_dynar_free(&stacks2);
+  xbt_dynar_free(&equals);

   return 0;
   
 }
   return 0;
   
 }


@@ -245,9 +302,13 @@ static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){
         }
       }
     }
         }
       }
     }

+    xbt_dynar_free(&s_tokens1);
+    xbt_dynar_free(&s_tokens2);

     cursor++;
   }
 
     cursor++;
   }
 

+  xbt_dynar_free(&tokens1);
+  xbt_dynar_free(&tokens2);

   return diff;
   
 }
   return diff;
   
 }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 2efb2d0..ce251a3 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -550,7 +550,7 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
   MC_SET_RAW_MEM;
   while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
 
   MC_SET_RAW_MEM;
   while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)

-    MC_pair_stateless_delete(pair);
+    pair_stateless_free(pair);

   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index d111368..f04ea98 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -217,12 +217,14 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 
 /********************* Double-DFS stateless *******************/
 
 
 /********************* 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);
 }
 
   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);
 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);


@@ -233,6 +235,19 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   return p;
 }
 
   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);
 void MC_ddfs_init(void){
 
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);


@@ -257,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 */
   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 
   /* Save the initial state */

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index af91f56..9c0f065 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -46,7 +46,7 @@ void MC_take_snapshot(mc_snapshot_t);
 void MC_take_snapshot_liveness(mc_snapshot_t s);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 void MC_take_snapshot_liveness(mc_snapshot_t s);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);

-
+void snapshot_stack_free_voidp(void *s);

 
 /********************************* MC Global **********************************/
 extern double *mc_time;
 
 /********************************* MC Global **********************************/
 extern double *mc_time;


@@ -243,6 +243,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
 void MC_pair_delete(mc_pair_t pair);
 void MC_exit_liveness(void);
 mc_state_t MC_state_pair_new(void);
 void MC_pair_delete(mc_pair_t pair);
 void MC_exit_liveness(void);
 mc_state_t MC_state_pair_new(void);

+void pair_reached_free(mc_pair_reached_t pair);
+void pair_reached_free_voidp(void *p);

 
 /* **** Double-DFS stateless **** */
 
 
 /* **** Double-DFS stateless **** */
 


@@ -257,7 +259,8 @@ void MC_ddfs_init(void);
 void MC_ddfs(int search_cycle);
 void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);
 void MC_ddfs(int search_cycle);
 void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);

-void MC_pair_stateless_delete(mc_pair_stateless_t pair);
+void pair_stateless_free(mc_pair_stateless_t pair);
+void pair_stateless_free_voidp(void *p);

 
 /********************************** Configuration of MC **************************************/
 extern xbt_fifo_t mc_stack_safety;
 
 /********************************** Configuration of MC **************************************/
 extern xbt_fifo_t mc_stack_safety;

diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c
index 97c397c..6cfff43 100644 (file)
--- a/src/xbt/automaton/automaton.c
+++ b/src/xbt/automaton/automaton.c
@@ -11,9 +11,9 @@
 xbt_automaton_t xbt_automaton_new(){
   xbt_automaton_t automaton = NULL;
   automaton = xbt_new0(struct xbt_automaton, 1);
 xbt_automaton_t xbt_automaton_new(){
   xbt_automaton_t automaton = NULL;
   automaton = xbt_new0(struct xbt_automaton, 1);

-  automaton->states = xbt_dynar_new(sizeof(xbt_state_t), NULL);
-  automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
-  automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), NULL);
+  automaton->states = xbt_dynar_new(sizeof(xbt_state_t), xbt_state_free_voidp);
+  automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
+  automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), xbt_propositional_symbol_free_voidp);

   return automaton;
 }
 
   return automaton;
 }
 


@@ -22,8 +22,8 @@ xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){
   state = xbt_new0(struct xbt_state, 1);
   state->type = type;
   state->id = strdup(id);
   state = xbt_new0(struct xbt_state, 1);
   state->type = type;
   state->id = strdup(id);

-  state->in = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
-  state->out = xbt_dynar_new(sizeof(xbt_transition_t), NULL); 
+  state->in = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
+  state->out = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); 

   xbt_dynar_push(a->states, &state);
   return state;
 }
   xbt_dynar_push(a->states, &state);
   return state;
 }


@@ -100,85 +100,6 @@ xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src
   return NULL;
 }
 
   return NULL;
 }
 

-void xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function){
-  unsigned int cursor = 0;
-  xbt_state_t state = NULL;
-  xbt_transition_t transition = NULL;
-
-  xbt_dynar_foreach(a->states, cursor, state){
-    xbt_dynar_free(&(state->out));
-    xbt_dynar_free(&(state->in));
-  }
-
-  xbt_dynar_foreach(a->transitions, cursor, transition){
-    if(transition_free_function) 
-      (*transition_free_function) (transition->label);
-  }
-
-  xbt_dynar_foreach(a->states, cursor, state)
-    free(state);
-  xbt_dynar_free(&(a->states));
-
-  xbt_dynar_foreach(a->transitions, cursor, state)
-    free(transition);
-  xbt_dynar_free(&(a->transitions));
-
-  free(a);
-
-  return;
-}
-
-void xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function){
-  unsigned long nbr;
-  unsigned long i;
-  unsigned int cursor = 0;
-  xbt_state_t state = NULL;
-  xbt_transition_t transition = NULL;
-
-  nbr = xbt_dynar_length(a->transitions);
-  for(i = 0; i <nbr; i++){
-    xbt_dynar_get_cpy(a->transitions, cursor, &transition);
-    if((transition->src == s) || (transition->dst == s)){
-      xbt_automaton_free_transition(a, transition, transition_free_function);
-    }else{
-      cursor++;
-    }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(a->states, cursor, state)
-    if(state == s)
-      xbt_dynar_cursor_rm(a->states, &cursor);
-
-  xbt_dynar_free(&(s->in));
-  xbt_dynar_free(&(s->out));
-
-  free(s);
-
-  return;
-}
-
-void xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function){
-  int index;
-  unsigned int cursor = 0;
-  xbt_transition_t transition = NULL;
-
-  if((transition_free_function) && (t->label))
-    (*transition_free_function) (t->label);
-
-  xbt_dynar_foreach(a->transitions, cursor, transition) {
-    if(transition == t){
-      index = __xbt_find_in_dynar(transition->dst->in, transition);
-      xbt_dynar_remove_at(transition->dst->in, index, NULL);
-      index = __xbt_find_in_dynar(transition->src->out, transition);
-      xbt_dynar_remove_at(transition->src->out, index, NULL);
-      xbt_dynar_cursor_rm(a->transitions, & cursor);
-      free(transition);
-      break;
-    }  
-  }
-} 
-

 xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){
   return t->src;
 }
 xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){
   return t->src;
 }


@@ -364,3 +285,84 @@ int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
 
   return 0;
 }
 
   return 0;
 }

+
+/************ Free functions ****************/
+
+static void xbt_transition_free(xbt_transition_t t);
+static void xbt_exp_label_free(xbt_exp_label_t e);
+static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps);
+
+void xbt_state_free(xbt_state_t s){
+  if(s){
+    xbt_free(s->id);
+    xbt_dynar_free(&(s->in));
+    xbt_dynar_free(&(s->out));
+    xbt_free(s);
+    s = NULL;
+  }
+}
+
+void xbt_state_free_voidp(void *s){
+  xbt_state_free((xbt_state_t) * (void **) s);
+}
+
+static void xbt_transition_free(xbt_transition_t t){
+  if(t){
+    xbt_exp_label_free(t->label);
+    xbt_free(t);
+    t = NULL;
+  }
+}
+
+void xbt_transition_free_voidp(void *t){
+  xbt_transition_free((xbt_transition_t) * (void **) t);
+}
+
+static void xbt_exp_label_free(xbt_exp_label_t e){
+  if(e){
+    switch(e->type){
+    case 0:
+    case 1:
+      xbt_exp_label_free(e->u.or_and.left_exp);
+      xbt_exp_label_free(e->u.or_and.right_exp);
+      break;
+    case 2:
+      xbt_exp_label_free(e->u.exp_not);
+      break;
+    case 3:
+      xbt_free(e->u.predicat);
+      break;
+    default:
+      break;
+    }
+    xbt_free(e);
+    e = NULL;
+  }
+}
+
+void xbt_exp_label_free_voidp(void *e){
+  xbt_exp_label_free((xbt_exp_label_t) * (void **) e);
+}
+
+static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){
+  if(ps){
+    xbt_free(ps->pred);
+    xbt_free(ps);
+    ps = NULL;
+  }
+}
+
+void xbt_propositional_symbol_free_voidp(void *ps){
+  xbt_propositional_symbol_free((xbt_propositional_symbol_t) * (void **) ps);
+}
+
+void xbt_automaton_free(xbt_automaton_t a){
+  if(a){
+    xbt_dynar_free(&(a->propositional_symbols));
+    xbt_dynar_free(&(a->transitions));
+    xbt_dynar_free(&(a->states));
+    xbt_state_free(a->current_state);
+    xbt_free(a);
+    a = NULL;
+  }
+}