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 112ffd8..ce2924e 100644 (file)
--- 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 1cbca27..503d498 100644 (file)
--- 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 caff24d..af91f56 100644 (file)
--- 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 {