diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 88e8b8893d14a439fefe504bf97a9e6ab47903c4..3acd478d3389ed3bf7c734af005e5a9b76a6f84d 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -25,6 +25,8 @@ Plugin E-ACSL <next-release> ############################ +-* E-ACSL [2020-07-09] Decrease the number of allocated blocks when one + block is freed. - E-ACSL [2020-06-19] Add support of bitwise operators for C integers. (frama-c/e-acsl#33) - E-ACSL [2020-06-19] Add support to create GMP rational from GMP 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 1a2bac5abefb1b9a9702e55e92dceef54b468cef..d2400f592b324ad670de36b215512328d12434f9 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 @@ -979,7 +979,7 @@ static void unset_heap_segment(void *ptr, int init, const char *function) { /* Nullify shadow block */ memset(base_shadow, ZERO, alloc_size); /* Adjust tracked allocation size */ - heap_allocation_size -= length; + update_heap_allocation(-length); #ifdef E_ACSL_TEMPORAL /*{{{*/ /* Nullify temporal shadow */ uintptr_t *t_base_shadow = (uintptr_t*)TEMPORAL_HEAP_SHADOW(ptr);