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 06095dee47a96f2533d37d21558ab2d76cbd7374..f33861a3036955206276f54332a318ce4a47b5f9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
@@ -6,65 +6,57 @@
#include <stdio.h>
#include <stdint.h>
-# ifndef UINTPTR_MAX
-# if __WORDSIZE == 64
-# define UINTPTR_MAX (18446744073709551615UL)
-# else
-# define UINTPTR_MAX (4294967295U)
-# endif
-# endif
-
extern size_t __e_acsl_heap_size;
int main(int argc, char **argv) {
- // Allocation increases
+ /* Allocation increases */
char *a = malloc(7);
/*@assert (__e_acsl_heap_size == 7); */
char *b = malloc(14);
/*@assert (__e_acsl_heap_size == 21); */
- // Allocation decreases
+ /* Allocation decreases */
free(a);
/*@assert (__e_acsl_heap_size == 14); */
- // Make sure that free with NULL behaves and does not affect allocation
+ /* Make sure that free with NULL behaves and does not affect allocation */
a = NULL;
free(a);
/*@assert (__e_acsl_heap_size == 14); */
- // Realloc decreases allocation
+ /* Realloc decreases allocation */
b = realloc(b, 9);
/*@assert (__e_acsl_heap_size == 9); */
- // Realloc increases allocation
+ /* Realloc increases allocation */
b = realloc(b, 18);
/*@assert (__e_acsl_heap_size == 18); */
- // Realloc with 0 is equivalent to free
+ /* Realloc with 0 is equivalent to free */
b = realloc(b, 0);
b = NULL;
/*@assert (__e_acsl_heap_size == 0); */
- // realloc with 0 is equivalent to malloc
+ /* realloc with 0 is equivalent to malloc */
b = realloc(b, 8);
/*@assert (__e_acsl_heap_size == 8); */
- // Abandon b and behave like malloc again
+ /* Abandon b and behave like malloc again */
b = realloc(NULL, 8);
/*@assert (__e_acsl_heap_size == 16); */
- // Make realloc fail by supplying a huge number
- b = realloc(NULL, UINTPTR_MAX);
+ /* Make realloc fail by supplying a huge number */
+ b = realloc(NULL, SIZE_MAX);
/*@assert (__e_acsl_heap_size == 16); */
/*@assert (b == NULL); */
- // Same as test for calloc ...
- b = calloc(UINTPTR_MAX,UINTPTR_MAX);
+ /* Same as test for calloc ... */
+ b = calloc(SIZE_MAX, SIZE_MAX);
/*@assert (__e_acsl_heap_size == 16); */
/*@assert (b == NULL); */
- // ... and for malloc
- b = malloc(UINTPTR_MAX);
+ /* ... and for malloc */
+ b = malloc(SIZE_MAX);
/*@assert (__e_acsl_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 68e399c55a9771097d53d1be20028dbd7988f4d5..e807b0f5f05c46ac84d9eced937eaa44e2dd5bed 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
@@ -8,62 +8,62 @@ int main(int argc, char **argv)
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",22);
+ (char *)"main",(char *)"__e_acsl_heap_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",24);
+ (char *)"main",(char *)"__e_acsl_heap_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",28);
+ (char *)"main",(char *)"__e_acsl_heap_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",33);
+ (char *)"main",(char *)"__e_acsl_heap_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",37);
+ (char *)"main",(char *)"__e_acsl_heap_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",41);
+ (char *)"main",(char *)"__e_acsl_heap_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",46);
+ (char *)"main",(char *)"__e_acsl_heap_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",50);
+ (char *)"main",(char *)"__e_acsl_heap_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",54);
+ (char *)"main",(char *)"__e_acsl_heap_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",58);
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",50);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
- (char *)"b == (char *)((void *)0)",59);
+ (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",63);
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",55);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
- (char *)"b == (char *)((void *)0)",64);
+ (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",68);
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",60);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
- (char *)"b == (char *)((void *)0)",69);
+ (char *)"b == (char *)((void *)0)",61);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
index 4e798da57d84d4de54832e897d426ae62b355d37..3bd9be96dfeb4b9109124c78fe60530b2cb50413 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
-tests/e-acsl-runtime/memsize.c:22:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/memsize.c:24:[value] warning: assertion got status invalid (stopping propagation).
+tests/e-acsl-runtime/memsize.c:14:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation).