model-checker : init equal_to field to -1 for each allocated block/fragment at the...

diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c
index a33b54a..ff2dbb7 100644 (file)
--- a/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@ -128,6 +128,35 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
   ignore_done = 0;
 
+  /* 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;
@@ -342,36 +371,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
   }
 
   XBT_DEBUG("Different blocks or fragments in heap2 : %d\n", nb_diff2);
-  
-  
-  /* Reset equal information */
-  i = 1;
-
-  while(i<heaplimit){
-    if(heapinfo1[i].type == 0){
-      heapinfo1[i].busy_block.equal_to = -1;
-    }
-    if(heapinfo1[i].type > 0){
-      for(j=0; j < MAX_FRAGMENT_PER_BLOCK; j++){
-        heapinfo1[i].busy_frag.equal_to[j] = -1;
-      }
-    }
-    i++; 
-  }
-
-  i = 1;
-
-  while(i<heaplimit){
-    if(heapinfo2[i].type == 0){
-      heapinfo2[i].busy_block.equal_to = -1;
-    }
-    if(heapinfo2[i].type > 0){
-      for(j=0; j < MAX_FRAGMENT_PER_BLOCK; j++){
-        heapinfo2[i].busy_frag.equal_to[j] = -1;
-      }
-    }
-    i++; 
-  }
 
   xbt_dynar_free(&previous);
  

diff --git a/src/xbt/mmalloc/mmalloc.c b/src/xbt/mmalloc/mmalloc.c
index cae6d37..e6f796d 100644 (file)
--- a/src/xbt/mmalloc/mmalloc.c
+++ b/src/xbt/mmalloc/mmalloc.c
@@ -153,7 +153,6 @@ void *mmalloc(xbt_mheap_t mdp, size_t size)
 
       frag_nb = RESIDUAL(result, BLOCKSIZE) >> log;
       mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = requested_size;
-      mdp->heapinfo[block].busy_frag.equal_to[frag_nb] = -1;
       xbt_backtrace_no_malloc(mdp->heapinfo[block].busy_frag.bt[frag_nb],XBT_BACKTRACE_SIZE);
 
       next->prev->next = next->next;
@@ -195,7 +194,6 @@ void *mmalloc(xbt_mheap_t mdp, size_t size)
         }
       }
       mdp->heapinfo[block].busy_frag.frag_size[0] = requested_size;
-      mdp->heapinfo[block].busy_frag.equal_to[0] = -1;
       xbt_backtrace_no_malloc(mdp->heapinfo[block].busy_frag.bt[0],XBT_BACKTRACE_SIZE);
       
       /* Initialize the nfree and first counters for this block.  */
@@ -245,7 +243,6 @@ void *mmalloc(xbt_mheap_t mdp, size_t size)
         block = BLOCK(result);
         for (it=0;it<blocks;it++){
           mdp->heapinfo[block+it].type = 0;
-          mdp->heapinfo[block+it].busy_block.equal_to = -1;
         }
         mdp->heapinfo[block].busy_block.size = blocks;
         mdp->heapinfo[block].busy_block.busy_size = requested_size;
@@ -283,7 +280,6 @@ void *mmalloc(xbt_mheap_t mdp, size_t size)
 
     for (it=0;it<blocks;it++){
       mdp->heapinfo[block+it].type = 0;
-      mdp->heapinfo[block+it].busy_block.equal_to = -1;
     }
     mdp->heapinfo[block].busy_block.size = blocks;
     mdp->heapinfo[block].busy_block.busy_size = requested_size;