Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : equal_to field of blocks/fragments updated twice with match_equals
[simgrid.git] / src / xbt / mmalloc / mm_diff.c
index f577979..3eb8b10 100644 (file)
@@ -13,8 +13,6 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
                                 "Logging specific to mm_diff in mmalloc");
 
-extern char *xbt_binary_name;
-
 xbt_dynar_t mc_heap_comparison_ignore;
 xbt_dynar_t stacks_areas;
 
@@ -59,7 +57,6 @@ void mmalloc_backtrace_block_display(void* heapinfo, int block){
       fprintf(stderr, "%d ---> %s\n",i, e.bt_strings[i] + 4);
     }
   }
-
 }
 
 void mmalloc_backtrace_fragment_display(void* heapinfo, int block, int frag){
@@ -113,7 +110,6 @@ void mmalloc_backtrace_display(void *addr){
     mmalloc_backtrace_fragment_display(heap->heapinfo, block, frag_nb);
     break;
   }
-
 }
 
 
@@ -188,6 +184,35 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac
     i2++; 
   }
 
+  /* Init equal information */
+  i1 = 1;
+
+  while(i1<=heaplimit){
+    if(heapinfo1[i1].type == 0){
+      heapinfo1[i1].busy_block.equal_to = -1;
+    }
+    if(heapinfo1[i1].type > 0){
+      for(j1=0; j1 < MAX_FRAGMENT_PER_BLOCK; j1++){
+        heapinfo1[i1].busy_frag.equal_to[j1] = -1;
+      }
+    }
+    i1++; 
+  }
+
+  i2 = 1;
+
+  while(i2<=heaplimit){
+    if(heapinfo2[i2].type == 0){
+      heapinfo2[i2].busy_block.equal_to = -1;
+    }
+    if(heapinfo2[i2].type > 0){
+      for(j2=0; j2 < MAX_FRAGMENT_PER_BLOCK; j2++){
+        heapinfo2[i2].busy_frag.equal_to[j2] = -1;
+      }
+    }
+    i2++; 
+  }
+
   /* Check busy blocks*/
 
   i1 = 1;
@@ -546,7 +571,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac
   heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
 
   return ((nb_diff1 > 0) || (nb_diff2 > 0));
-
 }
 
 static heap_area_t new_heap_area(int block, int fragment){