From d90a41491cfb04188c4469729fa60d01ec0ff693 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Sun, 18 Nov 2012 19:23:46 +0100 Subject: [PATCH] model-checker : improve stack ignore in heap comparison algorithm --- src/xbt/mmalloc/mm_diff.c | 35 +++++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 14 deletions(-) diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 9d0a154a85..d9ca5d61eb 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -212,6 +212,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac stack->process_name = strdup(stack_name); stack->size = heapinfo1[i1].busy_block.busy_size; xbt_dynar_push(*stack1, &stack); + res_compare = -1; } if(heapinfo1[i1].busy_block.busy_size == 0){ @@ -243,20 +244,23 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac stack->process_name = strdup(stack_name); stack->size = heapinfo2[current_block].busy_block.busy_size; xbt_dynar_push(*stack2, &stack); + res_compare = -1; } add_heap_area_pair(previous, current_block, -1, current_block, -1); - if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ - if(in_mc_comparison_ignore((int)current_block, -1)) - res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 1); - else + if(res_compare != -1){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ + if(in_mc_comparison_ignore((int)current_block, -1)) + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 1); + else + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 0); + }else{ res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 0); - }else{ - res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 0); + } } - if(res_compare == 0){ + if(res_compare == 0 || res_compare == -1){ for(k=1; k < heapinfo2[current_block].busy_block.size; k++) heapinfo2[current_block+k].busy_block.equal_to = new_heap_area(i1, -1); for(k=1; k < heapinfo1[current_block].busy_block.size; k++) @@ -285,6 +289,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac stack->process_name = strdup(stack_name); stack->size = heapinfo2[i2].busy_block.busy_size; xbt_dynar_push(*stack2, &stack); + res_compare = -1; } if(i2 == current_block){ @@ -315,16 +320,18 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac /* Comparison */ add_heap_area_pair(previous, i1, -1, i2, -1); - if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ - if(in_mc_comparison_ignore((int)i1, -1)) - res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 1); - else + if(res_compare != -1){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ + if(in_mc_comparison_ignore((int)i1, -1)) + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 1); + else + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0); + }else{ res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0); - }else{ - res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0); + } } - if(res_compare == 0){ + if(res_compare == 0 || res_compare == -1){ for(k=1; k < heapinfo2[i2].busy_block.size; k++) heapinfo2[i2+k].busy_block.equal_to = new_heap_area(i1, -1); for(k=1; k < heapinfo1[i1].busy_block.size; k++) -- 2.20.1