Change __e_acsl_heap_size to __e_acsl_heap_allocation_size to avoid

ambiguity in the segment-based shadow memory model of E-ACSL

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c

@@ -61,10 +61,10 @@ static const int nbr_bits_to_1[256] = {
 /**************************/
 /* HEAP USAGE         {{{ */
 /**************************/
-static size_t heap_size = 0;
+static size_t heap_allocation_size = 0;
 
-static size_t get_heap_size(void) {
-  return heap_size;
+static size_t get_heap_allocation_size(void) {
+  return heap_allocation_size;
 }
 /* }}} */
 
@@ -325,7 +325,7 @@ static void* bittree_malloc(size_t size) {
   void *res = native_malloc(size);
   if (res) {
     bt_block * new_block = store_block(res, size);
-    heap_size += size;
+    heap_allocation_size += size;
     new_block->freeable = true;
   }
   return res;
@@ -341,7 +341,7 @@ static void* bittree_calloc(size_t nbr_block, size_t size_block) {
   void *res = native_calloc(nbr_block, size_block);
   if (res) {
     bt_block * new_block = store_block(res, size);
-    heap_size += size;
+    heap_allocation_size += size;
     new_block->freeable = 1;
     /* Mark allocated block as freeable and initialized */
     new_block->init_bytes = size;
@@ -362,7 +362,7 @@ static void *bittree_aligned_alloc(size_t alignment, size_t size) {
   if (res) {
     bt_block * new_block = store_block(res, size);
     new_block->freeable = 1;
-    heap_size += size;
+    heap_allocation_size += size;
   }
   return res;
 }
@@ -383,7 +383,7 @@ static int bittree_posix_memalign(void **memptr, size_t alignment, size_t size)
   if (!res) {
     bt_block * new_block = store_block(*memptr, size);
     new_block->freeable = 1;
-    heap_size += size;
+    heap_allocation_size += size;
   }
   return res;
 }
@@ -405,7 +405,7 @@ static void* bittree_realloc(void* ptr, size_t size) {
   new_ptr = native_realloc((void*)tmp->ptr, size);
   if(new_ptr == NULL)
     return NULL;
-  heap_size -= tmp->size;
+  heap_allocation_size -= tmp->size;
   /* realloc changes start address -- re-enter the element */
   if (tmp->ptr != (uintptr_t)new_ptr) {
     bt_remove(tmp);
@@ -448,7 +448,7 @@ static void* bittree_realloc(void* ptr, size_t size) {
   }
   tmp->size = size;
   tmp->freeable = true;
-  heap_size += size;
+  heap_allocation_size += size;
   return (void*)tmp->ptr;
 }
 
@@ -460,7 +460,7 @@ static void bittree_free(void* ptr) {
   if (!res) {
     vabort("Not a start of block (%a) in free\n", ptr);
   } else {
-    heap_size -= res->size;
+    heap_allocation_size -= res->size;
     native_free(ptr);
     bt_clean_block_init(res);
     bt_remove(res);
@@ -582,8 +582,8 @@ public_alias(full_init)
 public_alias(memory_clean)
 public_alias(memory_init)
 /* Heap size */
-public_alias(get_heap_size)
-public_alias(heap_size)
+public_alias(get_heap_allocation_size)
+public_alias(heap_allocation_size)
 #ifdef E_ACSL_DEBUG /* Debug */
 public_alias(bt_print_block)
 public_alias(bt_print_tree)

src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h

@@ -193,14 +193,14 @@ void __e_acsl_memory_init(int *argc_ref, char ***argv, size_t ptr_size)
 
 /*! \brief Return the cumulative size (in bytes) of tracked heap allocation. */
 /*@ assigns \result \from __e_acsl_internal_heap; */
-size_t __e_acsl_get_heap_size(void)
+size_t __e_acsl_get_heap_allocation_size(void)
   __attribute__((FC_BUILTIN));
 
 /*! \brief A variable holding a cumulative size (in bytes) of tracked
  * heap allocation. */
-extern size_t __e_acsl_heap_size;
+extern size_t __e_acsl_heap_allocation_size;
 
 /*@ predicate diffSize{L1,L2}(integer i) =
-  \at(__e_acsl_heap_size, L1) - \at(__e_acsl_heap_size, L2) == i;
+  \at(__e_acsl_heap_allocation_size, L1) - \at(__e_acsl_heap_allocation_size, L2) == i;
 */
 #endif

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_store_block
 [value] using specification for function __e_acsl_full_init

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_store_block
 [value] using specification for function __e_acsl_full_init

src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
 [value] using specification for function __gmpz_init_set_str
 [value] using specification for function __gmpz_init_set_si

src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_neg

src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
   T1[0..2] ∈ {0}
   T2[0..3] ∈ {0}
 tests/gmp/array.i:10:[value] entering loop for the first time

src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
   T1[0..2] ∈ {0}
   T2[0..3] ∈ {0}
 tests/gmp/array.i:10:[value] entering loop for the first time

src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
   A ∈ {0}
 [value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_store_block

src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
   A ∈ {0}
 [value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_store_block

src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle

@@ -13,6 +13,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_get_si
 [value] using specification for function __gmpz_cmp

src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle

@@ -13,6 +13,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert

src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
 [value] using specification for function __gmpz_init_set_str
 [value] using specification for function __gmpz_cmp

src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert

src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
                  of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main).
                  Using specification of my_pow.

src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
                  of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main).
                  Using specification of my_pow.

src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle

@@ -13,6 +13,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle

@@ -13,7 +13,7 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
   __fc_wctomb_state ∈ {0}
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_size ∈ [--..--]
+  __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert