model-checker : check current heap

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 521b95a..0703b17 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -113,12 +113,16 @@ void MC_take_snapshot(mc_snapshot_t snapshot)
 }
 
 void MC_init_memory_map_info(){
+
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
   
   unsigned int i = 0;
   s_map_region_t reg;
   memory_map_t maps = get_memory_map();
 
-   while (i < maps->mapsize) {
+  while (i < maps->mapsize) {
     reg = maps->regions[i];
     if ((reg.prot & PROT_WRITE)){
       if (maps->regions[i].pathname == NULL){
@@ -144,6 +148,13 @@ void MC_init_memory_map_info(){
     }
     i++;
   }
+  
+  free_memory_map(maps);
+
+  MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 
 }
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 6c52e8b..0692a23 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -148,8 +148,6 @@ void MC_init_safety(void)
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
   
 }
 
@@ -166,6 +164,8 @@ void MC_modelcheck(void)
 }
 
 void MC_init_liveness(){
+
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
@@ -201,6 +201,9 @@ void MC_init_liveness(){
   get_libsimgrid_plt_section();
   get_binary_plt_section();
 
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+
 }
 
 void MC_modelcheck_liveness(){
@@ -567,8 +570,6 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
 
 }
 
@@ -654,8 +655,6 @@ void MC_automaton_load(const char *file){
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
 
 }
 
@@ -674,8 +673,6 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
   
 }
 
@@ -683,6 +680,8 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
 void MC_ignore(void *address, size_t size){
 
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
   MC_SET_RAW_MEM;
   
   if(mc_comparison_ignore == NULL)
@@ -715,10 +714,15 @@ void MC_ignore(void *address, size_t size){
   xbt_dynar_insert_at(mc_comparison_ignore, cursor, &region);
 
   MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 }
 
 void MC_new_stack_area(void *stack, char *name, void* context){
 
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
   MC_SET_RAW_MEM;
 
   if(stacks_areas == NULL)
@@ -732,6 +736,9 @@ void MC_new_stack_area(void *stack, char *name, void* context){
   xbt_dynar_push(stacks_areas, &region);
   
   MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 }
 
 /************ DWARF ***********/