Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : init equal_to field to -1 for each allocated block/fragment at the...
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 16 Aug 2012 22:13:52 +0000 (00:13 +0200)
committershenshei <paul.bedaride@gmail.com>
Tue, 27 Nov 2012 17:23:28 +0000 (18:23 +0100)
src/xbt/mmalloc/mm_diff.c

index 9ffeac1..166b0f7 100644 (file)
@@ -186,6 +186,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;
@@ -544,7 +573,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){