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 479c625ba84e645b463ef286f3685bba2d02c466..21985b94e1cd2eca4695e98af06be88476ce5e06 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 66b47387ada98ef2b3bfffc58c10198061a2bb3c..46a375dc46cf7548137a3ad8ea58c50c09f5b0d8 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 cb1f73c37efbaa26ab43fad70271e86d9458891e..b95faa854343f762a04eb0c96c4a996c769e2e9b 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 cb1f73c37efbaa26ab43fad70271e86d9458891e..b95faa854343f762a04eb0c96c4a996c769e2e9b 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 42f7150ee8dbcfb147854b3516846acd90bacc17..ef42a641f62119fbd93e0a78e78836cbad3f5a29 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 42da1827f9a9588ec2a436c49912b936a9255a9f..7cd3588f92f5b492bf7b55394c9d0e212e7101fd 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 d4b20b219996a1753ce540ededf1441648f098ef..1dc1420dc36b4479bde10caf5b85fd739adffa75 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 81a4b2d3c6d7b24635e7603eac9023cf7b05b060..abee4dc3c7a71ac96a286903d8979adf6699f8db 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 dd9c356abc741f47407fc8162b03b688f8b593cc..8a83d5c555e2abfcacc33f777b7b6d9ff5af5c9c 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 a4e92287d2f7841bcc4ceff64ec7e90d6ca11e50..6d02abba82808d0169a60118394903ed94c58d69 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 ada1d18071ab90f7cd24ca71d772c46414aec84d..6518cc1154c4d89c1089bd61d500d1f24b9b2504 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 ae71f63700135a7a29f3ca9561d1910de1acd86d..9baa5e8c7204ecee26b3f8f3ad4a41e36e4c748a 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 ada1d18071ab90f7cd24ca71d772c46414aec84d..6518cc1154c4d89c1089bd61d500d1f24b9b2504 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 9206f947b029e68c408a1c5f6b2bbc70e90304b2..e8c6147cea19c86bc2736082982591b9f33d5f58 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 749bb84a3e6181da6251379609baaa83a91d6e37..772dc0983f6270ed87500f8736e78a29b6822605 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 c5891ead6f5bd14167cc6b692b9a005ca2ed2868..7f54b3889e737e1ab673a886364ec34490cc79a1 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 26af2d5ab9cae019ba473beea8e5a30adc619415..e580bdf53e982d6e1be0d29987b028bb82e1573b 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 ed8716ac823f90633c137d2a3e7c9ead1f87400c..0eee735afc36e10a8119ed4869f16d99a6e405a2 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 ada1d18071ab90f7cd24ca71d772c46414aec84d..6518cc1154c4d89c1089bd61d500d1f24b9b2504 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 b0e5b6e32f832ae867fd789e82833f94a12f0782..1d4d29db8024b423de546c7bddd8f4535c3ddce2 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 3d03e693fa66f5c9a67301584a6ba17cb9d47f01..774cd469f6c06155636b3b9b45f082fb488953c2 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 663cef60518af74e17d2a682a062bde19d53e245..1c7ba24682cb42078a69ddaa8222b5a2ed1e6a12 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 7d7712fd8a49c4d6149e5cb0d7bc04e15ee0ea69..133c99f201d3abf69712aa1ea43009fa053e69eb 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 f33861a3036955206276f54332a318ce4a47b5f9..c214b60ebd4dcbb33a07b64bf3fddf3e7aec9a8e 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 e807b0f5f05c46ac84d9eced937eaa44e2dd5bed..c8dd172c9567096afe19ba398e4056bb3a423c1b 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);