diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h index 45fd1e1ab79accbe17ee651efeb9a8fe883a3d1f..3bc186850f953d816c87fb00107a50f2b441615b 100644 --- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h +++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h @@ -604,13 +604,13 @@ static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr) { length = short_lengths[code]; } +#ifndef E_ACSL_WEAK_VALIDITY if (addr != base_ptr) { - uintptr_t base_addr = addr - offset; - return BELONGS(base_ptr, base_addr, length) + return BELONGS(base_ptr, addr - offset, length) && offset + size <= length; - } else { - return offset + size <= length; } +#endif + return offset + size <= length; } return 0; } @@ -1053,8 +1053,12 @@ static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) { * offset is the difference between the address and base address (shadow[0]) * Then an address belongs to heap allocation if * offset + size <= length */ +#ifndef E_ACSL_WEAK_VALIDITY return base_shadow[0] == shadow[0] && (addr - shadow[0]) + size <= first_segment[1]; +#else + return (addr - shadow[0]) + size <= first_segment[1]; +#endif } return 0; }