X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/16161a9da50b5cd4bca163c8542a4d65ff78e7d1..6ab5d8cd5d2eaa1f52b6ec6b17ae12ca645854d1:/src/mc/compare.cpp diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp index d03dbfa44c..f302e81f87 100644 --- a/src/mc/compare.cpp +++ b/src/mc/compare.cpp @@ -151,12 +151,6 @@ static ssize_t heap_comparison_ignore_size(const std::vectorprocess().get_heap(); - return address >= heap->heapbase && address < heap->breakval; -} - static bool is_stack(const void *address) { for (auto const& stack : mc_model_checker->process().stack_areas()) @@ -260,10 +254,7 @@ static bool mmalloc_heap_differ(simgrid::mc::StateComparator& state, const simgr continue; } - if (heapinfo1->type < 0) { - fprintf(stderr, "Unkown mmalloc block type.\n"); - abort(); - } + xbt_assert(heapinfo1->type >= 0, "Unkown mmalloc block type: %d", heapinfo1->type); void* addr_block1 = ((void*)(((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase)); @@ -377,10 +368,7 @@ static bool mmalloc_heap_differ(simgrid::mc::StateComparator& state, const simgr continue; } - if (heapinfo2b->type < 0) { - fprintf(stderr, "Unknown mmalloc block type.\n"); - abort(); - } + xbt_assert(heapinfo2b->type >= 0, "Unkown mmalloc block type: %d", heapinfo2b->type); for (size_t j2 = 0; j2 < (size_t)(BLOCKSIZE >> heapinfo2b->type); j2++) { @@ -501,15 +489,15 @@ static bool heap_area_differ_without_type(simgrid::mc::StateComparator& state, c 1) != 0) { int pointer_align = (i / sizeof(void *)) * sizeof(void *); - const void* addr_pointed1 = snapshot1.read(remote((void**)((const char*)real_area1 + pointer_align))); - const void* addr_pointed2 = snapshot2.read(remote((void**)((const char*)real_area2 + pointer_align))); + const void* addr_pointed1 = snapshot1.read(remote((void* const*)((const char*)real_area1 + pointer_align))); + const void* addr_pointed2 = snapshot2.read(remote((void* const*)((const char*)real_area2 + pointer_align))); if (process.in_maestro_stack(remote(addr_pointed1)) && process.in_maestro_stack(remote(addr_pointed2))) { i = pointer_align + sizeof(void *); continue; } - if (is_on_heap(addr_pointed1) && is_on_heap(addr_pointed2)) { + if (snapshot1.on_heap(addr_pointed1) && snapshot2.on_heap(addr_pointed2)) { // Both addresses are in the heap: if (heap_area_differ(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, nullptr, 0)) return true; @@ -651,7 +639,7 @@ static bool heap_area_differ_with_type(simgrid::mc::StateComparator& state, cons if (pointer_level <= 1) { addr_pointed1 = snapshot1.read(remote((void* const*)real_area1)); addr_pointed2 = snapshot2.read(remote((void* const*)real_area2)); - if (is_on_heap(addr_pointed1) && is_on_heap(addr_pointed2)) + if (snapshot1.on_heap(addr_pointed1) && snapshot2.on_heap(addr_pointed2)) return heap_area_differ(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, type->subtype, pointer_level); else @@ -660,7 +648,7 @@ static bool heap_area_differ_with_type(simgrid::mc::StateComparator& state, cons for (size_t i = 0; i < (area_size / sizeof(void*)); i++) { addr_pointed1 = snapshot1.read(remote((void* const*)((const char*)real_area1 + i * sizeof(void*)))); addr_pointed2 = snapshot2.read(remote((void* const*)((const char*)real_area2 + i * sizeof(void*)))); - bool differ = is_on_heap(addr_pointed1) && is_on_heap(addr_pointed2) + bool differ = snapshot1.on_heap(addr_pointed1) && snapshot2.on_heap(addr_pointed2) ? heap_area_differ(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, type->subtype, pointer_level) : addr_pointed1 != addr_pointed2; @@ -700,9 +688,7 @@ static bool heap_area_differ_with_type(simgrid::mc::StateComparator& state, cons default: THROW_IMPOSSIBLE; - break; } - return false; } /** Infer the type of a part of the block from the type of the block @@ -1105,8 +1091,8 @@ static bool areas_differ_with_type(simgrid::mc::StateComparator& state, const vo } for (i = 0; i < type->element_count; i++) { size_t off = i * elm_size; - if (areas_differ_with_type(state, (char*)real_area1 + off, snapshot1, region1, (char*)real_area2 + off, - snapshot2, region2, type->subtype, pointer_level)) + if (areas_differ_with_type(state, (const char*)real_area1 + off, snapshot1, region1, + (const char*)real_area2 + off, snapshot2, region2, type->subtype, pointer_level)) return true; } break; @@ -1132,8 +1118,8 @@ static bool areas_differ_with_type(simgrid::mc::StateComparator& state, const vo // * a pointer leads to the read-only segment of the current object // * a pointer lead to a different ELF object - if (is_on_heap(addr_pointed1)) { - if (not is_on_heap(addr_pointed2)) + if (snapshot1.on_heap(addr_pointed1)) { + if (not snapshot2.on_heap(addr_pointed2)) return true; // The pointers are both in the heap: return simgrid::mc::heap_area_differ(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, nullptr,