Merge branch 'bugfix/basile/eacsl-fix-deallocation-tracking' into 'master'

[eacsl:runtime] Fix tracking of deallocation

See merge request frama-c/frama-c!2749

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

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);