From: Marion Guthmuller Date: Sun, 18 Nov 2012 18:23:46 +0000 (+0100) Subject: model-checker : improve stack ignore in heap comparison algorithm X-Git-Tag: v3_9_rc1~91^2~71 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d90a41491cfb04188c4469729fa60d01ec0ff693?hp=247d96de592ac1fcd59411032c6528f238764516 model-checker : improve stack ignore in heap comparison algorithm --- 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++)