diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c index 2cb37870059b5b46414ff525c8e2c8115ef83c13..c5c2d6a44fbea7812e73a0b96024fb4ebcf7f89d 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c +++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c @@ -13,7 +13,6 @@ int main(int argc, char const **argv) int res2 = posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15); /*@ assert Eva: initialization: \initialized(memptr); */ - /*@ assert Eva: mem_access: \valid_read(memptr); */ char *p = *memptr; __e_acsl_store_block((void *)(& p),(size_t)8); __e_acsl_full_init((void *)(& p)); diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle index 763ce72a19e897ad1af1bd400afa352a65673d42..505c3a9513d560559bd6786634c1d6a699413323 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle @@ -1,9 +1,7 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[kernel:annot:missing-spec] tests/runtime/memalign.c:12: Warning: - Neither code nor specification for function posix_memalign, generating default assigns from the prototype +[eva:alarm] tests/runtime/memalign.c:12: Warning: + function posix_memalign: precondition 'valid_memptr' got status unknown. [eva:alarm] tests/runtime/memalign.c:14: Warning: accessing uninitialized left-value. assert \initialized(memptr); -[eva:alarm] tests/runtime/memalign.c:14: Warning: - out of bounds read. assert \valid_read(memptr); [scope:rm_asserts] removing 2 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/test_config b/src/plugins/e-acsl/tests/runtime/test_config index 3d07f7500426e9ee476265cd446000213411b753..49e3e5e1028f11fde69f1e65163604f33b658af8 100644 --- a/src/plugins/e-acsl/tests/runtime/test_config +++ b/src/plugins/e-acsl/tests/runtime/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0 +OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0 -eva-warn-key libc:unsupported-spec=inactive EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@"