From accde0314e0070c6b19d6396e19b34ef58a965a9 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 24 Nov 2016 15:53:02 +0100
Subject: [PATCH] Change __e_acsl_heap_size to __e_acsl_heap_allocation_size
to avoid ambiguity in the segment-based shadow memory model of E-ACSL
---
.../bittree_model/e_acsl_bittree_mmodel.c | 24 +++---
.../e-acsl/share/e-acsl/e_acsl_mmodel_api.h | 6 +-
.../full-mmodel/oracle/addrOf.0.res.oracle | 2 +-
.../full-mmodel/oracle/addrOf.1.res.oracle | 2 +-
.../tests/gmp/oracle/arith.0.res.oracle | 2 +-
.../tests/gmp/oracle/arith.1.res.oracle | 2 +-
.../tests/gmp/oracle/array.0.res.oracle | 2 +-
.../tests/gmp/oracle/array.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/at.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/at.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/cast.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/cast.1.res.oracle | 2 +-
.../tests/gmp/oracle/comparison.0.res.oracle | 2 +-
.../tests/gmp/oracle/comparison.1.res.oracle | 2 +-
.../gmp/oracle/integer_constant.0.res.oracle | 2 +-
.../gmp/oracle/integer_constant.1.res.oracle | 2 +-
.../tests/gmp/oracle/longlong.0.res.oracle | 2 +-
.../tests/gmp/oracle/longlong.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/not.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/not.1.res.oracle | 2 +-
.../tests/gmp/oracle/quantif.0.res.oracle | 2 +-
.../tests/gmp/oracle/quantif.1.res.oracle | 2 +-
.../e-acsl/tests/runtime/init_function.c | 4 +-
src/plugins/e-acsl/tests/runtime/memsize.c | 26 +++---
.../e-acsl/tests/runtime/oracle/gen_memsize.c | 84 +++++++++++--------
25 files changed, 98 insertions(+), 86 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 479c625ba84..21985b94e1c 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/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)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 66b47387ada..46a375dc46c 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/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
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
index cb1f73c37ef..b95faa85434 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
index cb1f73c37ef..b95faa85434 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index 42f7150ee8d..ef42a641f62 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
index 42da1827f9a..7cd3588f92f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
index d4b20b21999..1dc1420dc36 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
index 81a4b2d3c6d..abee4dc3c7a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
index dd9c356abc7..8a83d5c555e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
index a4e92287d2f..6d02abba828 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index ada1d18071a..6518cc1154c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index ae71f637001..9baa5e8c720 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
index ada1d18071a..6518cc1154c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index 9206f947b02..e8c6147cea1 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
index 749bb84a3e6..772dc0983f6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index c5891ead6f5..7f54b3889e7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 26af2d5ab9c..e580bdf53e9 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index ed8716ac823..0eee735afc3 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
index ada1d18071a..6518cc1154c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index b0e5b6e32f8..1d4d29db802 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index 3d03e693fa6..774cd469f6c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.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/quantif.i:9:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:9:[value] entering loop for the first time
[value] using specification for function __e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 663cef60518..1c7ba24682c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.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/quantif.i:9:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_init_set_si
diff --git a/src/plugins/e-acsl/tests/runtime/init_function.c b/src/plugins/e-acsl/tests/runtime/init_function.c
index 7d7712fd8a4..133c99f201d 100644
--- a/src/plugins/e-acsl/tests/runtime/init_function.c
+++ b/src/plugins/e-acsl/tests/runtime/init_function.c
@@ -7,7 +7,7 @@
#include <stdlib.h>
int main(void) {
- /* @assert (__heap_size == 0); */
+ /* @assert (__heap_allocation_size == 0); */
char *a = malloc(7);
- /* @assert (__heap_size == 7); */
+ /* @assert (__heap_allocation_size == 7); */
}
diff --git a/src/plugins/e-acsl/tests/runtime/memsize.c b/src/plugins/e-acsl/tests/runtime/memsize.c
index f33861a3036..c214b60ebd4 100644
--- a/src/plugins/e-acsl/tests/runtime/memsize.c
+++ b/src/plugins/e-acsl/tests/runtime/memsize.c
@@ -6,58 +6,58 @@
#include <stdio.h>
#include <stdint.h>
-extern size_t __e_acsl_heap_size;
+extern size_t __e_acsl_heap_allocation_size;
int main(int argc, char **argv) {
/* Allocation increases */
char *a = malloc(7);
- /*@assert (__e_acsl_heap_size == 7); */
+ /*@assert (__e_acsl_heap_allocation_size == 7); */
char *b = malloc(14);
- /*@assert (__e_acsl_heap_size == 21); */
+ /*@assert (__e_acsl_heap_allocation_size == 21); */
/* Allocation decreases */
free(a);
- /*@assert (__e_acsl_heap_size == 14); */
+ /*@assert (__e_acsl_heap_allocation_size == 14); */
/* Make sure that free with NULL behaves and does not affect allocation */
a = NULL;
free(a);
- /*@assert (__e_acsl_heap_size == 14); */
+ /*@assert (__e_acsl_heap_allocation_size == 14); */
/* Realloc decreases allocation */
b = realloc(b, 9);
- /*@assert (__e_acsl_heap_size == 9); */
+ /*@assert (__e_acsl_heap_allocation_size == 9); */
/* Realloc increases allocation */
b = realloc(b, 18);
- /*@assert (__e_acsl_heap_size == 18); */
+ /*@assert (__e_acsl_heap_allocation_size == 18); */
/* Realloc with 0 is equivalent to free */
b = realloc(b, 0);
b = NULL;
- /*@assert (__e_acsl_heap_size == 0); */
+ /*@assert (__e_acsl_heap_allocation_size == 0); */
/* realloc with 0 is equivalent to malloc */
b = realloc(b, 8);
- /*@assert (__e_acsl_heap_size == 8); */
+ /*@assert (__e_acsl_heap_allocation_size == 8); */
/* Abandon b and behave like malloc again */
b = realloc(NULL, 8);
- /*@assert (__e_acsl_heap_size == 16); */
+ /*@assert (__e_acsl_heap_allocation_size == 16); */
/* Make realloc fail by supplying a huge number */
b = realloc(NULL, SIZE_MAX);
- /*@assert (__e_acsl_heap_size == 16); */
+ /*@assert (__e_acsl_heap_allocation_size == 16); */
/*@assert (b == NULL); */
/* Same as test for calloc ... */
b = calloc(SIZE_MAX, SIZE_MAX);
- /*@assert (__e_acsl_heap_size == 16); */
+ /*@assert (__e_acsl_heap_allocation_size == 16); */
/*@assert (b == NULL); */
/* ... and for malloc */
b = malloc(SIZE_MAX);
- /*@assert (__e_acsl_heap_size == 16); */
+ /*@assert (__e_acsl_heap_allocation_size == 16); */
/*@assert (b == NULL); */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
index e807b0f5f05..c8dd172c956 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
@@ -6,61 +6,73 @@ int main(int argc, char **argv)
char *b;
__e_acsl_memory_init(& argc,& argv,8UL);
a = (char *)malloc((unsigned long)7);
- /*@ assert __e_acsl_heap_size ≡ 7; */
- __e_acsl_assert(__e_acsl_heap_size == 7UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 7",14);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 7; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 7",14);
b = (char *)malloc((unsigned long)14);
- /*@ assert __e_acsl_heap_size ≡ 21; */
- __e_acsl_assert(__e_acsl_heap_size == 21UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 21",16);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 21; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 21UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 21",16);
free((void *)a);
- /*@ assert __e_acsl_heap_size ≡ 14; */
- __e_acsl_assert(__e_acsl_heap_size == 14UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 14",20);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 14; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 14",20);
a = (char *)0;
free((void *)a);
- /*@ assert __e_acsl_heap_size ≡ 14; */
- __e_acsl_assert(__e_acsl_heap_size == 14UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 14",25);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 14; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 14",25);
b = (char *)realloc((void *)b,(unsigned long)9);
- /*@ assert __e_acsl_heap_size ≡ 9; */
- __e_acsl_assert(__e_acsl_heap_size == 9UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 9",29);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 9; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 9UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 9",29);
b = (char *)realloc((void *)b,(unsigned long)18);
- /*@ assert __e_acsl_heap_size ≡ 18; */
- __e_acsl_assert(__e_acsl_heap_size == 18UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 18",33);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 18; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 18UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 18",33);
b = (char *)realloc((void *)b,(unsigned long)0);
b = (char *)0;
- /*@ assert __e_acsl_heap_size ≡ 0; */
- __e_acsl_assert(__e_acsl_heap_size == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 0",38);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 0; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 0",38);
b = (char *)realloc((void *)b,(unsigned long)8);
- /*@ assert __e_acsl_heap_size ≡ 8; */
- __e_acsl_assert(__e_acsl_heap_size == 8UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 8",42);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 8; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 8UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 8",42);
b = (char *)realloc((void *)0,(unsigned long)8);
- /*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 16",46);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 16; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 16",46);
b = (char *)realloc((void *)0,18446744073709551615UL);
- /*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 16",50);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 16; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 16",50);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",51);
b = (char *)calloc(18446744073709551615UL,18446744073709551615UL);
- /*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 16",55);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 16; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 16",55);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",56);
b = (char *)malloc(18446744073709551615UL);
- /*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 16",60);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 16; */
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,(char *)"Assertion",
+ (char *)"main",
+ (char *)"__e_acsl_heap_allocation_size == 16",60);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",61);
--
GitLab