model-checker : init equal_to in mmalloc info

diff --git a/src/xbt/mmalloc/mfree.c b/src/xbt/mmalloc/mfree.c
index ad5e05e..2472c91 100644 (file)
--- a/src/xbt/mmalloc/mfree.c
+++ b/src/xbt/mmalloc/mfree.c
@@ -168,7 +168,9 @@ void mfree(struct mdesc *mdp, void *ptr)
 
     /* Set size used in the fragment to -1 */
     mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = -1;
 
     /* Set size used in the fragment to -1 */
     mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = -1;

-    
+    mdp->heapinfo[block].busy_frag.ignore[frag_nb] = 0;
+    mdp->heapinfo[block].busy_frag.equal_to[frag_nb] = NULL;
+

 //    fprintf(stderr,"nfree:%zu capa:%d\n", mdp->heapinfo[block].busy_frag.nfree,(BLOCKSIZE >> type));
     if (mdp->heapinfo[block].busy_frag.nfree ==
         (BLOCKSIZE >> type) - 1) {
 //    fprintf(stderr,"nfree:%zu capa:%d\n", mdp->heapinfo[block].busy_frag.nfree,(BLOCKSIZE >> type));
     if (mdp->heapinfo[block].busy_frag.nfree ==
         (BLOCKSIZE >> type) - 1) {


@@ -179,6 +181,7 @@ void mfree(struct mdesc *mdp, void *ptr)
       mdp->heapinfo[block].type = 0;
       mdp->heapinfo[block].busy_block.size = 1;
       mdp->heapinfo[block].busy_block.busy_size = 0;
       mdp->heapinfo[block].type = 0;
       mdp->heapinfo[block].busy_block.size = 1;
       mdp->heapinfo[block].busy_block.busy_size = 0;

+      mdp->heapinfo[block].busy_block.equal_to = NULL;

             
       /* Keep the statistics accurate.  */
       mdp -> heapstats.chunks_used++;
             
       /* Keep the statistics accurate.  */
       mdp -> heapstats.chunks_used++;

diff --git a/src/xbt/mmalloc/mmalloc.c b/src/xbt/mmalloc/mmalloc.c
index 04f6731..9e94017 100644 (file)
--- a/src/xbt/mmalloc/mmalloc.c
+++ b/src/xbt/mmalloc/mmalloc.c
@@ -117,13 +117,14 @@ static void *register_morecore(struct mdesc *mdp, size_t size)
 
     /* mark the space previously occupied by the block info as free by first marking it
      * as occupied in the regular way, and then freing it */
 
     /* mark the space previously occupied by the block info as free by first marking it
      * as occupied in the regular way, and then freing it */

-    for (it=0; it<BLOCKIFY(mdp->heapsize * sizeof(malloc_info)); it++)
+    for (it=0; it<BLOCKIFY(mdp->heapsize * sizeof(malloc_info)); it++){

       newinfo[BLOCK(oldinfo)+it].type = 0;
       newinfo[BLOCK(oldinfo)+it].type = 0;

+      newinfo[BLOCK(oldinfo)+it].busy_block.ignore = 0;
+      newinfo[BLOCK(oldinfo+it)].busy_block.equal_to = NULL;
+    }

 
     newinfo[BLOCK(oldinfo)].busy_block.size = BLOCKIFY(mdp->heapsize * sizeof(malloc_info));
     newinfo[BLOCK(oldinfo)].busy_block.busy_size = size;
 
     newinfo[BLOCK(oldinfo)].busy_block.size = BLOCKIFY(mdp->heapsize * sizeof(malloc_info));
     newinfo[BLOCK(oldinfo)].busy_block.busy_size = size;

-    newinfo[BLOCK(oldinfo)].busy_block.ignore = 0;
-    newinfo[BLOCK(oldinfo)].busy_block.equal_to = NULL;

     //newinfo[BLOCK(oldinfo)].busy_block.bt_size = 0;// FIXME setup the backtrace
     mfree(mdp, (void *) oldinfo);
     mdp->heapsize = newsize;
     //newinfo[BLOCK(oldinfo)].busy_block.bt_size = 0;// FIXME setup the backtrace
     mfree(mdp, (void *) oldinfo);
     mdp->heapsize = newsize;

diff --git a/src/xbt/mmalloc/mrealloc.c b/src/xbt/mmalloc/mrealloc.c
index dc31fa1..7cbe32c 100644 (file)
--- a/src/xbt/mmalloc/mrealloc.c
+++ b/src/xbt/mmalloc/mrealloc.c
@@ -82,8 +82,11 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
       int it;
       /* The new size is smaller; return excess memory to the free list. */
       //printf("(%s) return excess memory...",xbt_thread_self_name());
       int it;
       /* The new size is smaller; return excess memory to the free list. */
       //printf("(%s) return excess memory...",xbt_thread_self_name());

-      for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++)
+      for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++){

         mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here
         mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here

+        mdp->heapinfo[it].busy_block.ignore = 0;
+        mdp->heapinfo[it].busy_block.equal_to = NULL;
+      }

 
       mdp->heapinfo[block + blocks].busy_block.size
         = mdp->heapinfo[block].busy_block.size - blocks;
 
       mdp->heapinfo[block + blocks].busy_block.size
         = mdp->heapinfo[block].busy_block.size - blocks;