From fea228d813dfd7399f94d6b11299226f629172de Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 17 Aug 2012 00:13:52 +0200 Subject: [PATCH] model-checker : init equal_to field to -1 for each allocated block/fragment at the beginning of the heap comparison --- src/xbt/mmalloc/mm_diff.c | 59 +++++++++++++++++++-------------------- src/xbt/mmalloc/mmalloc.c | 4 --- 2 files changed, 29 insertions(+), 34 deletions(-) diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index a33b54a872..ff2dbb7847 100644 --- 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 0){ - for(j=0; j < MAX_FRAGMENT_PER_BLOCK; j++){ - heapinfo1[i].busy_frag.equal_to[j] = -1; - } - } - i++; - } - - i = 1; - - while(i 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 cae6d3701e..e6f796dbc5 100644 --- 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;itheapinfo[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;itheapinfo[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; -- 2.20.1