From 26595e9fc41101a70102ff0a6f30849eaeb0318f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 19 Jan 2021 18:04:11 +0100
Subject: [PATCH] [eacsl] Update tests
---
src/plugins/e-acsl/tests/memory/memsize.c | 3 +-
.../tests/memory/oracle_ci/gen_memalign.c | 6 ++
.../tests/memory/oracle_ci/gen_memsize.c | 30 ++++-----
.../tests/memory/oracle_ci/memsize.res.oracle | 67 +++++++++++++++++--
4 files changed, 86 insertions(+), 20 deletions(-)
diff --git a/src/plugins/e-acsl/tests/memory/memsize.c b/src/plugins/e-acsl/tests/memory/memsize.c
index c214b60ebd4..2260a306878 100644
--- a/src/plugins/e-acsl/tests/memory/memsize.c
+++ b/src/plugins/e-acsl/tests/memory/memsize.c
@@ -1,5 +1,6 @@
-/* run.config
+/* run.config_ci
COMMENT: Checking heap memory size
+ STDOPT: +"-eva-no-builtins-auto"
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
index 594eb809025..86b350d6bcd 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
@@ -40,6 +40,12 @@ extern int __e_acsl_sound_verdict;
*/
int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size);
+/*@ assigns __e_acsl_heap_allocation_size, __e_acsl_heap_allocated_blocks;
+ assigns __e_acsl_heap_allocation_size
+ \from (indirect: alignment), size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks
+ \from (indirect: alignment), size, __e_acsl_heap_allocated_blocks;
+ */
void *aligned_alloc(size_t alignment, size_t size);
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index 134e80f8daf..d31fa69d2a5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -11,73 +11,73 @@ int main(int argc, char **argv)
char *a = malloc((unsigned long)7);
__e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 7",
- "tests/memory/memsize.c",14);
+ "tests/memory/memsize.c",15);
/*@ assert __e_acsl_heap_allocation_size ≡ 7; */ ;
char *b = malloc((unsigned long)14);
__e_acsl_assert(__e_acsl_heap_allocation_size == 21UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 21",
- "tests/memory/memsize.c",16);
+ "tests/memory/memsize.c",17);
/*@ assert __e_acsl_heap_allocation_size ≡ 21; */ ;
free((void *)a);
__e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 14",
- "tests/memory/memsize.c",20);
+ "tests/memory/memsize.c",21);
/*@ assert __e_acsl_heap_allocation_size ≡ 14; */ ;
a = (char *)0;
free((void *)a);
__e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 14",
- "tests/memory/memsize.c",25);
+ "tests/memory/memsize.c",26);
/*@ assert __e_acsl_heap_allocation_size ≡ 14; */ ;
b = (char *)realloc((void *)b,(unsigned long)9);
__e_acsl_assert(__e_acsl_heap_allocation_size == 9UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 9",
- "tests/memory/memsize.c",29);
+ "tests/memory/memsize.c",30);
/*@ assert __e_acsl_heap_allocation_size ≡ 9; */ ;
b = (char *)realloc((void *)b,(unsigned long)18);
__e_acsl_assert(__e_acsl_heap_allocation_size == 18UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 18",
- "tests/memory/memsize.c",33);
+ "tests/memory/memsize.c",34);
/*@ assert __e_acsl_heap_allocation_size ≡ 18; */ ;
b = (char *)realloc((void *)b,(unsigned long)0);
b = (char *)0;
__e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 0",
- "tests/memory/memsize.c",38);
+ "tests/memory/memsize.c",39);
/*@ assert __e_acsl_heap_allocation_size ≡ 0; */ ;
b = (char *)realloc((void *)b,(unsigned long)8);
__e_acsl_assert(__e_acsl_heap_allocation_size == 8UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 8",
- "tests/memory/memsize.c",42);
+ "tests/memory/memsize.c",43);
/*@ assert __e_acsl_heap_allocation_size ≡ 8; */ ;
b = (char *)realloc((void *)0,(unsigned long)8);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",46);
+ "tests/memory/memsize.c",47);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
b = (char *)realloc((void *)0,18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",50);
+ "tests/memory/memsize.c",51);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
__e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
- "tests/memory/memsize.c",51);
+ "tests/memory/memsize.c",52);
/*@ assert b ≡ (char *)0; */ ;
b = (char *)calloc(18446744073709551615UL,18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",55);
+ "tests/memory/memsize.c",56);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
__e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
- "tests/memory/memsize.c",56);
+ "tests/memory/memsize.c",57);
/*@ assert b ≡ (char *)0; */ ;
b = (char *)malloc(18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",60);
+ "tests/memory/memsize.c",61);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
__e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
- "tests/memory/memsize.c",61);
+ "tests/memory/memsize.c",62);
/*@ assert b ≡ (char *)0; */ ;
__retres = 0;
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
index 2db55f248cb..68e3cc47739 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
@@ -1,7 +1,66 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/memsize.c:14: Warning:
+[eva] tests/memory/memsize.c:14: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:15: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:16: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:17: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:17: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:20: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:20: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:21: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:25: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:26: Warning: assertion got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:452: Warning:
+ no 'assigns \result \from ...' clause specified for function realloc
+[eva] tests/memory/memsize.c:29: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:29: Warning:
+ function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:30: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:33: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:33: Warning:
+ function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:34: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:37: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:37: Warning:
+ function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:39: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:39: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:42: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:43: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:43: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:46: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:47: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:50: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:51: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:51: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:52: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:385: Warning:
+ no 'assigns \result \from ...' clause specified for function calloc
+[eva] tests/memory/memsize.c:55: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:56: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:56: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:60: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:61: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:61: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:62: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/memsize.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/memory/memsize.c:16: Warning:
- function __e_acsl_assert: precondition got status invalid.
--
GitLab