From c52b2c7af6f378e89d776fffdfb1a091b63fd4c5 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 18 Feb 2016 10:49:57 +0100
Subject: [PATCH] [tests] Fixed memsize test to use __heap_size instead of
__memory_size
---
.../e-acsl/tests/e-acsl-runtime/memsize.c | 26 +++----
.../tests/e-acsl-runtime/oracle/gen_memsize.c | 74 +++++++++----------
2 files changed, 49 insertions(+), 51 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
index f4e3c0b89d7..8322d7982c1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
@@ -14,58 +14,58 @@
# endif
# endif
-extern size_t __memory_size;
+extern size_t __heap_size;
int main(int argc, char **argv) {
// Allocation increases
char *a = malloc(7);
- /*@assert (__memory_size == 7); */
+ /*@assert (__heap_size == 7); */
char *b = malloc(14);
- /*@assert (__memory_size == 21); */
+ /*@assert (__heap_size == 21); */
// Allocation decreases
free(a);
- /*@assert (__memory_size == 14); */
+ /*@assert (__heap_size == 14); */
// Make sure that free with NULL behaves and does not affect allocation
a = NULL;
free(a);
- /*@assert (__memory_size == 14); */
+ /*@assert (__heap_size == 14); */
// Realloc decreases allocation
b = realloc(b, 9);
- /*@assert (__memory_size == 9); */
+ /*@assert (__heap_size == 9); */
// Realloc increases allocation
b = realloc(b, 18);
- /*@assert (__memory_size == 18); */
+ /*@assert (__heap_size == 18); */
// Realloc with 0 is equivalent to free
b = realloc(b, 0);
b = NULL;
- /*@assert (__memory_size == 0); */
+ /*@assert (__heap_size == 0); */
// realloc with 0 is equivalent to malloc
b = realloc(b, 8);
- /*@assert (__memory_size == 8); */
+ /*@assert (__heap_size == 8); */
// Abandon b and behave like malloc again
b = realloc(NULL, 8);
- /*@assert (__memory_size == 16); */
+ /*@assert (__heap_size == 16); */
// Make realloc fail by supplying a huge number
b = realloc(NULL, UINTPTR_MAX);
- /*@assert (__memory_size == 16); */
+ /*@assert (__heap_size == 16); */
/*@assert (b == NULL); */
// Same as test for calloc ...
b = calloc(UINTPTR_MAX,UINTPTR_MAX);
- /*@assert (__memory_size == 16); */
+ /*@assert (__heap_size == 16); */
/*@assert (b == NULL); */
// ... and for malloc
b = malloc(UINTPTR_MAX);
- /*@assert (__memory_size == 16); */
+ /*@assert (__heap_size == 16); */
/*@assert (b == NULL); */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
index 831f2e7b7eb..6451ce34d79 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
@@ -1,6 +1,4 @@
/* Generated by Frama-C */
-extern size_t __memory_size;
-
int main(int argc, char **argv)
{
int __retres;
@@ -11,72 +9,72 @@ int main(int argc, char **argv)
__store_block((void *)(& a),8UL);
__full_init((void *)(& a));
a = (char *)__e_acsl_malloc((unsigned long)7);
- /*@ assert __memory_size ≡ 7; */
- e_acsl_assert(__memory_size == (unsigned long)7,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 7",22);
+ /*@ assert __heap_size ≡ 7; */
+ e_acsl_assert(__heap_size == (unsigned long)7,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 7",22);
__full_init((void *)(& b));
b = (char *)__e_acsl_malloc((unsigned long)14);
- /*@ assert __memory_size ≡ 21; */
- e_acsl_assert(__memory_size == (unsigned long)21,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 21",24);
+ /*@ assert __heap_size ≡ 21; */
+ e_acsl_assert(__heap_size == (unsigned long)21,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 21",24);
__e_acsl_free((void *)a);
- /*@ assert __memory_size ≡ 14; */
- e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 14",28);
+ /*@ assert __heap_size ≡ 14; */
+ e_acsl_assert(__heap_size == (unsigned long)14,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 14",28);
__full_init((void *)(& a));
a = (char *)0;
__e_acsl_free((void *)a);
- /*@ assert __memory_size ≡ 14; */
- e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 14",33);
+ /*@ assert __heap_size ≡ 14; */
+ e_acsl_assert(__heap_size == (unsigned long)14,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 14",33);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)9);
- /*@ assert __memory_size ≡ 9; */
- e_acsl_assert(__memory_size == (unsigned long)9,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 9",37);
+ /*@ assert __heap_size ≡ 9; */
+ e_acsl_assert(__heap_size == (unsigned long)9,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 9",37);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)18);
- /*@ assert __memory_size ≡ 18; */
- e_acsl_assert(__memory_size == (unsigned long)18,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 18",41);
+ /*@ assert __heap_size ≡ 18; */
+ e_acsl_assert(__heap_size == (unsigned long)18,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 18",41);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)0);
__full_init((void *)(& b));
b = (char *)0;
- /*@ assert __memory_size ≡ 0; */
- e_acsl_assert(__memory_size == (unsigned long)0,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 0",46);
+ /*@ assert __heap_size ≡ 0; */
+ e_acsl_assert(__heap_size == (unsigned long)0,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 0",46);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)8);
- /*@ assert __memory_size ≡ 8; */
- e_acsl_assert(__memory_size == (unsigned long)8,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 8",50);
+ /*@ assert __heap_size ≡ 8; */
+ e_acsl_assert(__heap_size == (unsigned long)8,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 8",50);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)0,(unsigned long)8);
- /*@ assert __memory_size ≡ 16; */
- e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 16",54);
+ /*@ assert __heap_size ≡ 16; */
+ e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 16",54);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)0,18446744073709551615UL);
- /*@ assert __memory_size ≡ 16; */
- e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 16",58);
+ /*@ assert __heap_size ≡ 16; */
+ e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 16",58);
/*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",59);
__full_init((void *)(& b));
b = (char *)__calloc(18446744073709551615UL,18446744073709551615UL);
- /*@ assert __memory_size ≡ 16; */
- e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 16",63);
+ /*@ assert __heap_size ≡ 16; */
+ e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 16",63);
/*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",64);
__full_init((void *)(& b));
b = (char *)__e_acsl_malloc(18446744073709551615UL);
- /*@ assert __memory_size ≡ 16; */
- e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
- (char *)"main",(char *)"__memory_size == 16",68);
+ /*@ assert __heap_size ≡ 16; */
+ e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__heap_size == 16",68);
/*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",69);
--
GitLab