model-checker : free memory

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 307e3ea..656541b 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -53,6 +53,10 @@ void stack_region_free_voidp(void *s);
 
 void heap_ignore_region_free(mc_heap_ignore_region_t r);
 void heap_ignore_region_free_voidp(void *r);
+void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v);
+void data_bss_ignore_variable_free_voidp(void *v);
+void stack_ignore_variable_free(mc_stack_ignore_variable_t v);
+void stack_ignore_variable_free_voidp(void *v);
 
 SG_END_DECL()
 #endif                          /* _MC_MC_H */

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index a89b14a..8f7a23d 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -231,6 +231,7 @@ void MC_free_snapshot(mc_snapshot_t snapshot)
   for(i=0; i < NB_REGIONS; i++)
     MC_region_destroy(snapshot->regions[i]);
 
+  xbt_free(snapshot->stack_sizes);
   xbt_dynar_free(&(snapshot->stacks));
   xbt_dynar_free(&(snapshot->to_ignore));
   xbt_free(snapshot);
@@ -500,6 +501,7 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
 
             if(!xbt_dynar_is_empty(compose)){
               frame_pointer_address = xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1, variable_value_t)->value.address ; 
+              xbt_dynar_reset(compose);
             }
             break;
           default :
@@ -566,6 +568,7 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
                 xbt_free(to_append);
               }
             }
+            xbt_dynar_reset(compose);
           }else{
             to_append = bprintf("%s=undefined\n", current_variable->name);
             xbt_strbuff_append(variables, to_append);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index bb5f942..d30d69f 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -936,6 +936,14 @@ void MC_remove_ignore_heap(void *address, size_t size){
 
 }
 
+void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
+  xbt_free(v);
+}
+
+void data_bss_ignore_variable_free_voidp(void *v){
+  data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
+}
+
 void MC_ignore_data_bss(void *address, size_t size){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -943,7 +951,7 @@ void MC_ignore_data_bss(void *address, size_t size){
   MC_SET_RAW_MEM;
   
   if(mc_data_bss_comparison_ignore == NULL)
-    mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), NULL);
+    mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
 
   mc_data_bss_ignore_variable_t var = NULL;
   var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
@@ -965,6 +973,7 @@ void MC_ignore_data_bss(void *address, size_t size){
       cursor = (start + end) / 2;
       current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
       if(current_var->address == address){
+        data_bss_ignore_variable_free(var);
         MC_UNSET_RAW_MEM;
         if(raw_mem_set)
           MC_SET_RAW_MEM;
@@ -1041,7 +1050,15 @@ static size_t data_bss_ignore_size(void *address){
   return 0;
 }
 
+void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
+  xbt_free(v->var_name);
+  xbt_free(v->frame);
+  xbt_free(v);
+}
 
+void stack_ignore_variable_free_voidp(void *v){
+  stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
+}
 
 void MC_ignore_stack(const char *var_name, const char *frame_name){
   
@@ -1050,15 +1067,15 @@ void MC_ignore_stack(const char *var_name, const char *frame_name){
   MC_SET_RAW_MEM;
 
   if(mc_stack_comparison_ignore == NULL)
-    mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), NULL);
-
+    mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
+  
+  mc_stack_ignore_variable_t var = NULL;
+  var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
+  var->var_name = strdup(var_name);
+  var->frame = strdup(frame_name);
+  
   if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
 
-    mc_stack_ignore_variable_t var = NULL;
-    var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
-    var->var_name = strdup(var_name);
-    var->frame = strdup(frame_name);
-
     xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
 
   }else{
@@ -1073,6 +1090,7 @@ void MC_ignore_stack(const char *var_name, const char *frame_name){
       current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
       if(strcmp(current_var->frame, frame_name) == 0){
         if(strcmp(current_var->var_name, var_name) == 0){
+          stack_ignore_variable_free(var);
           MC_UNSET_RAW_MEM;
           if(raw_mem_set)
             MC_SET_RAW_MEM;
@@ -1089,11 +1107,6 @@ void MC_ignore_stack(const char *var_name, const char *frame_name){
         end = cursor - 1;
     }
 
-    mc_stack_ignore_variable_t var = NULL;
-    var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
-    var->var_name = strdup(var_name);
-    var->frame = strdup(frame_name);
-
     if(strcmp(current_var->frame, frame_name) < 0)
       xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
     else

diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c
index b0e84a6..04538dd 100644 (file)
--- a/src/mc/memory_map.c
+++ b/src/mc/memory_map.c
@@ -161,5 +161,6 @@ void free_memory_map(memory_map_t map){
   for(i=0; i< map->mapsize; i++){
     xbt_free(map->regions[i].pathname);
   }
+  xbt_free(map->regions);
   xbt_free(map);
 }