From b7cda16062db95bf02082d9a10c7156befd9e739 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 27 Mar 2017 18:36:29 +0200
Subject: [PATCH] synchronize with frama-c/frama-c!1214
---
src/plugins/e-acsl/tests/bts/bts1390.c | 1 +
.../e-acsl/tests/bts/oracle/bts1390.res.oracle | 6 +++---
src/plugins/e-acsl/tests/runtime/initialized.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_memalign.c | 1 +
.../runtime/oracle/initialized.res.oracle | 18 +++++++++---------
.../tests/runtime/oracle/mainargs.res.oracle | 3 ++-
.../tests/runtime/oracle/memalign.res.oracle | 14 +-------------
.../tests/runtime/oracle/offset.res.oracle | 10 ----------
8 files changed, 18 insertions(+), 36 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
index 74cba86cdbe..eddb97a0285 100644
--- a/src/plugins/e-acsl/tests/bts/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,4 +1,5 @@
/* run.config
+ STDOPT: +"-no-val-builtins-auto"
COMMENT: bts #1390, issue with typing of quantified variables
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index 5882e8efc73..077c0847b43 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:12:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:17:[value] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
diff --git a/src/plugins/e-acsl/tests/runtime/initialized.c b/src/plugins/e-acsl/tests/runtime/initialized.c
index e417de91b82..44ca8c15992 100644
--- a/src/plugins/e-acsl/tests/runtime/initialized.c
+++ b/src/plugins/e-acsl/tests/runtime/initialized.c
@@ -1,4 +1,5 @@
/* run.config
+ STDOPT: +"-no-val-builtins-auto"
COMMENT: Behaviours of the \initialized E-ACSL predicate
*/
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 50a7e1ed59c..ed712a0a824 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -11,6 +11,7 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& memptr));
int res2 =
posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+ /*@ assert Value: initialisation: \initialized(memptr); */
/*@ assert Value: mem_access: \valid_read(memptr); */
char *p = *memptr;
__e_acsl_store_block((void *)(& p),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index f882a082af8..442101a5faa 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -1,16 +1,16 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/initialized.c:65:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:69:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
FRAMAC_SHARE/libc/stdlib.h:347:[value] warning: function realloc: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:362:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
-tests/runtime/initialized.c:74:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:76:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:75:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:77:[value] warning: assertion got status unknown.
FRAMAC_SHARE/libc/stdlib.h:334:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
-tests/runtime/initialized.c:84:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:93:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:96:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:107:[value] warning: out of bounds write. assert \valid(partsi + i);
-tests/runtime/initialized.c:105:[value] warning: out of bounds write. assert \valid(partsc + i);
+tests/runtime/initialized.c:86:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:97:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:108:[value] warning: out of bounds write. assert \valid(partsi + i);
+tests/runtime/initialized.c:106:[value] warning: out of bounds write. assert \valid(partsc + i);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index 1bc1d7077e2..e3f9a03de82 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -17,7 +17,8 @@ tests/runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_r
tests/runtime/mainargs.c:16:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv + argc);
FRAMAC_SHARE/libc/string.h:92:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:92:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly reading indeterminate data
+ invalid base: NULL
FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
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 45502e59bd2..4ba26f48cd6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
@@ -1,17 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
+tests/runtime/memalign.c:14:[value] warning: accessing uninitialized left-value. assert \initialized(memptr);
tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
-tests/runtime/memalign.c:15:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/memalign.c:16:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:17:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:334:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
-tests/runtime/memalign.c:19:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
-tests/runtime/memalign.c:23:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:26:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:29:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:32:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:33:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:34:[value] warning: assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
index 7924f9d3b38..efd02631129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
@@ -1,12 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-tests/runtime/offset.c:39:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/offset.c:40:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:41:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:43:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:44:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:49:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:51:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:53:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:55:[value] warning: assertion got status unknown.
--
GitLab