#include "xbt/str.h"
#include "mc/mc.h"
#include "xbt/mmalloc.h"
+#include "mc_object_info.h"
#include "mc/datatypes.h"
#include "mc/mc_private.h"
+#include "mc/mc_snapshot.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
"Logging specific to mc_diff in mc");
xbt_dynar_t mc_heap_comparison_ignore;
xbt_dynar_t stacks_areas;
-void *maestro_stack_start, *maestro_stack_end;
+
/********************************* Backtrace ***********************************/
mc_mem_region_t heap_region2 = snapshot2->regions[0];
// This is in snapshot do not use them directly:
- malloc_info* heapinfos1 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot1, MC_NO_PROCESS_INDEX);
- malloc_info* heapinfos2 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot2, MC_NO_PROCESS_INDEX);
+ malloc_info* heapinfos1 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot1, MC_NO_PROCESS_INDEX);
+ malloc_info* heapinfos2 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot2, MC_NO_PROCESS_INDEX);
while (i1 <= state->heaplimit) {
malloc_info* heapinfo2 = mc_snapshot_read_region(&heapinfos2[i1], heap_region2, &heapinfo_temp2, sizeof(malloc_info));
if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) { /* Free block */
- i1 += heapinfo1->free_block.size;
+ i1 ++;
continue;
}
malloc_info* heapinfo2b = mc_snapshot_read_region(&heapinfos2[i2], heap_region2, &heapinfo_temp2b, sizeof(malloc_info));
if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
- i2 += heapinfo2b->free_block.size;
+ i2 ++;
+ continue;
+ }
+
+ // We currently do not match fragments with unfragmented blocks (maybe we should).
+ if (heapinfo2b->type == MMALLOC_TYPE_UNFRAGMENTED) {
+ i2++;
continue;
}
xbt_dynar_t previous, int size,
int check_ignore)
{
+ mc_process_t process = &mc_model_checker->process;
int i = 0;
void *addr_pointed1, *addr_pointed2;
addr_pointed1 = mc_snapshot_read_pointer((char *) real_area1 + pointer_align, snapshot1, process_index);
addr_pointed2 = mc_snapshot_read_pointer((char *) real_area2 + pointer_align, snapshot2, process_index);
- if (addr_pointed1 > maestro_stack_start
- && addr_pointed1 < maestro_stack_end
- && addr_pointed2 > maestro_stack_start
- && addr_pointed2 < maestro_stack_end) {
+ if (addr_pointed1 > process->maestro_stack_start
+ && addr_pointed1 < process->maestro_stack_end
+ && addr_pointed2 > process->maestro_stack_start
+ && addr_pointed2 < process->maestro_stack_end) {
i = pointer_align + sizeof(void *);
continue;
} else if (addr_pointed1 > state->s_heap
int match_pairs = 0;
- malloc_info* heapinfos1 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot1, process_index);
- malloc_info* heapinfos2 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot2, process_index);
+ malloc_info* heapinfos1 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot1, process_index);
+ malloc_info* heapinfos2 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot2, process_index);
malloc_info heapinfo_temp1, heapinfo_temp2;