From 9acdf60879cb316d1c06141c686b77cb2ea93cf1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 6 Aug 2020 11:29:17 +0200
Subject: [PATCH] [e-acsl:tests] update tests
---
.../oracle_ci/gen_bts1386_complex_flowgraph.c | 1 +
.../e-acsl/tests/bts/oracle_ci/gen_bts1398.c | 1 +
.../tests/bts/oracle_ci/gen_issue-eacsl-91.c | 27 ----
.../tests/full-mmodel/oracle_ci/gen_addrOf.c | 27 ----
.../tests/memory/oracle_ci/gen_constructor.c | 1 +
.../e-acsl/tests/memory/oracle_ci/gen_errno.c | 1 +
.../tests/memory/oracle_ci/gen_local_goto.c | 1 +
.../tests/memory/oracle_ci/gen_mainargs.c | 1 +
.../tests/memory/oracle_ci/gen_memalign.c | 121 +++++++++++++++++-
.../tests/memory/oracle_ci/gen_memsize.c | 2 +
.../tests/memory/oracle_ci/gen_stdout.c | 1 +
.../memory/oracle_ci/memalign.res.oracle | 29 +++++
.../e-acsl/tests/special/e-acsl-valid.c | 2 +-
.../tests/temporal/oracle_ci/gen_t_args.c | 1 +
.../temporal/oracle_ci/gen_t_local_init.c | 1 +
.../tests/temporal/oracle_ci/gen_t_memcpy.c | 1 +
16 files changed, 162 insertions(+), 56 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
index 5f3956f765f..b3d1e5df6a1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void duffcopy(char *to, char *from, int count)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
index 6c992808644..8f4aa78a777 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
index 519c77cc7f1..14dd1ab575a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
@@ -36,24 +36,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& b));
__e_acsl_store_block((void *)(& a),(size_t)2);
__e_acsl_full_init((void *)(& a));
- __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_tmpnam));
- __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
- __e_acsl_full_init((void *)(& __fc_tmpnam));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdin),(size_t)8);
- __e_acsl_full_init((void *)(& stdin));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
}
return;
}
@@ -62,15 +44,6 @@ void __e_acsl_globals_delete(void)
{
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& a));
- __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
- __e_acsl_delete_block((void *)(__fc_tmpnam));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index e7da245320f..574d904ff3e 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
@@ -35,24 +35,6 @@ void __e_acsl_globals_init(void)
__e_acsl_already_run = 1;
__e_acsl_store_block((void *)(& f),(size_t)1);
__e_acsl_full_init((void *)(& f));
- __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_tmpnam));
- __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
- __e_acsl_full_init((void *)(& __fc_tmpnam));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdin),(size_t)8);
- __e_acsl_full_init((void *)(& stdin));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
}
return;
}
@@ -60,15 +42,6 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_delete(void)
{
__e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
- __e_acsl_delete_block((void *)(__fc_tmpnam));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
index 15a99b43c04..4e43d7e9cff 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
index cc458e4e367..f38474ba466 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
@@ -1,5 +1,6 @@
/* Generated by Frama-C */
#include "errno.h"
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
index 2cf1cc44c0c..3d26e79512a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
index cd9cd223bf6..86e9de27822 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.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 7e7362461bb..f0a98343e01 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
@@ -1,6 +1,46 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
+/*@ requires valid_memptr: \valid(memptr);
+ requires
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+ allocates *\old(memptr);
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+ ensures result_zero: \result ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(size);
+ ensures result_non_zero: \result < 0 ∨ \result > 0;
+ assigns \result;
+ assigns \result \from (indirect: alignment);
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size);
+
+void *aligned_alloc(size_t alignment, size_t size);
+
int main(int argc, char const **argv)
{
int __retres;
@@ -11,7 +51,8 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& memptr),(size_t)8);
__e_acsl_full_init((void *)(& memptr));
int res2 =
- posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+ __gen_e_acsl_posix_memalign((void **)memptr,(unsigned long)256,
+ (unsigned long)15);
/*@ assert Eva: initialization: \initialized(memptr); */
char *p = *memptr;
__e_acsl_store_block((void *)(& p),(size_t)8);
@@ -138,4 +179,82 @@ int main(int argc, char const **argv)
return __retres;
}
+/*@ requires valid_memptr: \valid(memptr);
+ requires
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+ allocates *\old(memptr);
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+ ensures result_zero: \result ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(size);
+ ensures result_non_zero: \result < 0 ∨ \result > 0;
+ assigns \result;
+ assigns \result \from (indirect: alignment);
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
+{
+ int __retres;
+ {
+ int __gen_e_acsl_valid;
+ int __gen_e_acsl_and;
+ __e_acsl_store_block((void *)(& memptr),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)memptr,sizeof(void *),
+ (void *)memptr,(void *)(& memptr));
+ __e_acsl_assert(__gen_e_acsl_valid,"Precondition","posix_memalign",
+ "\\valid(memptr)","FRAMAC_SHARE/libc/stdlib.h",666);
+ if (alignment >= 8UL) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_band;
+ unsigned long __gen_e_acsl__3;
+ __gmpz_init_set_ui(__gen_e_acsl_,alignment);
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_band);
+ __gmpz_and(__gen_e_acsl_band,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_band));
+ __gen_e_acsl_and = __gen_e_acsl__3 == 0UL;
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_band);
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,"Precondition","posix_memalign",
+ "alignment >= sizeof(void *) &&\n((size_t)alignment & ((size_t)alignment - 1)) == 0",
+ "FRAMAC_SHARE/libc/stdlib.h",668);
+ }
+ __retres = posix_memalign(memptr,alignment,size);
+ __e_acsl_delete_block((void *)(& memptr));
+ return __retres;
+}
+
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 60fc5642381..afc1d47904c 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
@@ -1,6 +1,8 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern size_t __e_acsl_heap_allocation_size;
+
int main(int argc, char **argv)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
index 49ec6cf163e..75bddabfbe9 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
index 674eddac861..bcfe10a812c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
@@ -1,4 +1,33 @@
[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `posix_memalign':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] tests/memory/memalign.c:38: Warning:
+ E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/memory/memalign.c:38: Warning:
+ E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:669: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
+ E-ACSL construct `predicate performing read accesses' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning:
+ E-ACSL construct `predicate performing read accesses' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:668: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+ ignoring unsupported \allocates clause
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:679: Warning:
+ function __gen_e_acsl_posix_memalign, behavior allocation: postcondition 'allocation' got status unknown.
[eva:alarm] tests/memory/memalign.c:14: Warning:
accessing uninitialized left-value. assert \initialized(memptr);
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-valid.c b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
index f13f228682c..f84464d0075 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
@@ -1,6 +1,6 @@
/* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-no-valid
- STDOPT: #"@MACHDEP@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid"
+ STDOPT: #"@GLOBAL@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid"
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -eva -eva-verbose 0
MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid
*/
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
index 666d954b82b..3e24ef3f308 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
index 9ccb27aa258..00745623824 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_4;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
index 0f86c7371d4..3b0511fa9b1 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
--
GitLab