From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 17 Oct 2012 13:34:49 +0000 (+0200)
Subject: model-checker : ignore pointers on raw_heap in data segment libsimgrid comparison
X-Git-Tag: v3_9_rc1~91^2~186
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/5e80b119f85e258080482cb688a6b89e01d74595

model-checker : ignore pointers on raw_heap in data segment libsimgrid comparison
---

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 112ffd83ad..ce2924e14d 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -20,6 +20,7 @@ void *start_plt_binary, *end_plt_binary;
 char *libsimgrid_path;
 void *start_data_libsimgrid;
 void *start_text_binary;
+void *end_raw_heap;
 
 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size);
 static void MC_region_restore(mc_mem_region_t reg);
@@ -127,6 +128,8 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
           MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
           heap = snapshot->regions[nb_reg]->data;
           nb_reg++;
+        }else if(reg.start_addr == raw_heap){
+          end_raw_heap = reg.end_addr;
         }
         i++;
       } else {
diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 1cbca27975..503d498941 100644
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -82,6 +82,8 @@ static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
       addr_pointed2 = *((void **)((char *)d2 + pointer_align));
       if((addr_pointed1 > start_plt_libsimgrid && addr_pointed1 < end_plt_libsimgrid) || (addr_pointed2 > start_plt_libsimgrid && addr_pointed2 < end_plt_libsimgrid)){
         continue;
+      }else if(addr_pointed1 >= raw_heap && addr_pointed1 <= end_raw_heap && addr_pointed2 >= raw_heap && addr_pointed2 <= end_raw_heap){
+        continue;
       }else{
         XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in data libsimgrid region", i, (char *)d1 + i, (char *)d2 + i);
         XBT_DEBUG("Addresses pointed : %p - %p\n", addr_pointed1, addr_pointed2);
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index caff24d421..af91f56019 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -193,6 +193,7 @@ void get_libsimgrid_plt_section(void);
 void get_binary_plt_section(void);
 
 extern void *start_data_libsimgrid;
+extern void *end_raw_heap;
 
 /********************************** DPOR for safety  **************************************/
 typedef enum {