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 5f3956f765f048f6cac3858217ecfd51bfe4f7ea..b3d1e5df6a10a1ce8fb80e3003fc4f942cdff13b 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 6c992808644dc2b1a22a287bec261511fb770b8d..8f4aa78a77722c4c1bc7163cc8680bf7cc800d3a 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 519c77cc7f1e326c2caa8402207cbea2b6564600..14dd1ab575af5a0d4560ecc5a1ac7ae3bc49a5d3 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 e7da245320f44ca617784993e0bf842400a92cff..574d904ff3e9f01ffb34f47c1945664f8330ef7b 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 15a99b43c04dacb8866abecb8ce0ef28e7db4bbf..4e43d7e9cff59e04b077b46a1e9d90fc81d9e076 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 cc458e4e367b7f4f52387e3d42d727f7ff9f4df6..f38474ba466e667532e9d52c1e92653513013858 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 2cf1cc44c0cd0dd389bce183c8fa9c4fdb3ef873..3d26e79512a996e7a619a62f0c495e06bb09a0ee 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 cd9cd223bf692bfcd3df82812937c41f4ebd306e..86e9de278227b7ff043988d6464c7b6120e761ae 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 7e7362461bb1ec5e09bc5b26370fcda40ddbc4c3..f0a98343e01d91146897001094205c0d8d01a50e 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 60fc5642381eca2bf0accc0e9093530f27e8f3c0..afc1d47904c708484482355ef4be0aaf6fcd4c2b 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 49ec6cf163ec5ba0edfad147a4fa237e95bb0678..75bddabfbe9edd97d7bff4bac71129cf540e7428 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 674eddac861dff410a723d4a8016853a5ce17ca5..bcfe10a812c72940b682369df2ac5f11caaaecba 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 f13f228682c83508233deaaafcab494f4b811707..f84464d00758640dd8187876d1d0cd3bcefbcf50 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 666d954b82bcc4f6965b8b8b575a7f5f11c3a01e..3e24ef3f308c7f68f1fb6accf0ea4b6e604afe72 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 9ccb27aa258ca9cd5f58e030f4523d3535aec27f..007456238249612053c6ccc263073ada9d9840ba 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 0f86c7371d4c879dc64808a673a75ca10dbe1a7a..3b0511fa9b1b81d990817fb3c5eb74072f572a8d 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"