X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5cb8ea43b1c50f1cbe66b9a3ab2654aadad484c4..6c9922204dbafacbc6d1cc25d519f7c9a46c96e9:/src/mc/mc_diff.c

diff --git a/src/mc/mc_diff.c b/src/mc/mc_diff.c
index bbda6d5bd4..2566334954 100644
--- a/src/mc/mc_diff.c
+++ b/src/mc/mc_diff.c
@@ -10,15 +10,17 @@
 #include "xbt/str.h"
 #include "mc/mc.h"
 #include "xbt/mmalloc.h"
+#include "mc_object_info.h"
 #include "mc/datatypes.h"
 #include "mc/mc_private.h"
+#include "mc/mc_snapshot.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
                                 "Logging specific to mc_diff in mc");
 
 xbt_dynar_t mc_heap_comparison_ignore;
 xbt_dynar_t stacks_areas;
-void *maestro_stack_start, *maestro_stack_end;
+
 
 
 /********************************* Backtrace ***********************************/
@@ -436,8 +438,8 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   mc_mem_region_t heap_region2 = snapshot2->regions[0];
 
   // This is in snapshot do not use them directly:
-  malloc_info* heapinfos1 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot1, MC_NO_PROCESS_INDEX);
-  malloc_info* heapinfos2 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot2, MC_NO_PROCESS_INDEX);
+  malloc_info* heapinfos1 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot1, MC_NO_PROCESS_INDEX);
+  malloc_info* heapinfos2 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot2, MC_NO_PROCESS_INDEX);
 
   while (i1 <= state->heaplimit) {
 
@@ -445,7 +447,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
     malloc_info* heapinfo2 = mc_snapshot_read_region(&heapinfos2[i1], heap_region2, &heapinfo_temp2, sizeof(malloc_info));
 
     if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) {      /* Free block */
-      i1 += heapinfo1->free_block.size;
+      i1 ++;
       continue;
     }
 
@@ -596,7 +598,13 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
           malloc_info* heapinfo2b = mc_snapshot_read_region(&heapinfos2[i2], heap_region2, &heapinfo_temp2b, sizeof(malloc_info));
 
           if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
-            i2 += heapinfo2b->free_block.size;
+            i2 ++;
+            continue;
+          }
+
+          // We currently do not match fragments with unfragmented blocks (maybe we should).
+          if (heapinfo2b->type == MMALLOC_TYPE_UNFRAGMENTED) {
+            i2++;
             continue;
           }
 
@@ -761,6 +769,7 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, int process_i
                                           xbt_dynar_t previous, int size,
                                           int check_ignore)
 {
+  mc_process_t process = &mc_model_checker->process;
 
   int i = 0;
   void *addr_pointed1, *addr_pointed2;
@@ -797,10 +806,10 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, int process_i
       addr_pointed1 = mc_snapshot_read_pointer((char *) real_area1 + pointer_align, snapshot1, process_index);
       addr_pointed2 = mc_snapshot_read_pointer((char *) real_area2 + pointer_align, snapshot2, process_index);
 
-      if (addr_pointed1 > maestro_stack_start
-          && addr_pointed1 < maestro_stack_end
-          && addr_pointed2 > maestro_stack_start
-          && addr_pointed2 < maestro_stack_end) {
+      if (addr_pointed1 > process->maestro_stack_start
+          && addr_pointed1 < process->maestro_stack_end
+          && addr_pointed2 > process->maestro_stack_start
+          && addr_pointed2 < process->maestro_stack_end) {
         i = pointer_align + sizeof(void *);
         continue;
       } else if (addr_pointed1 > state->s_heap
@@ -1130,8 +1139,8 @@ int compare_heap_area(int process_index, void *area1, void *area2, mc_snapshot_t
 
   int match_pairs = 0;
 
-  malloc_info* heapinfos1 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot1, process_index);
-  malloc_info* heapinfos2 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot2, process_index);
+  malloc_info* heapinfos1 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot1, process_index);
+  malloc_info* heapinfos2 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot2, process_index);
 
   malloc_info heapinfo_temp1, heapinfo_temp2;