From 814e52d1a8fb46f1df0357f20c1f662a4cb545db Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 3 Feb 2016 08:23:11 +0100
Subject: [PATCH] [tests] update wrt libc changes
---
.../e-acsl-runtime/oracle/mainargs.0.res.oracle | 14 +++++++-------
.../e-acsl-runtime/oracle/mainargs.1.res.oracle | 10 +++++-----
2 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
index bd90eaf199b..db7d99e671c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
@@ -2,11 +2,11 @@
[e-acsl] warning: annotating undefined function `strlen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:90:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
+FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -37,12 +37,12 @@ tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
[value] using specification for function __initialized
tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
-FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
[value] using specification for function strlen
-FRAMAC_SHARE/libc/string.h:88:[value] Function strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:88:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
+FRAMAC_SHARE/libc/string.h:91:[value] Function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/string.h:90:[value] Function __e_acsl_strlen: postcondition got status unknown.
+FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown.
tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
index 52e0b30ccc7..d3b2a7b1d26 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -6,7 +6,7 @@ tests/e-acsl-runtime/mainargs.c:9:[e-acsl] warning: E-ACSL construct `logic func
Ignoring annotation.
tests/e-acsl-runtime/mainargs.c:9:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:90:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
+FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -61,12 +61,12 @@ tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
[value] using specification for function __initialized
tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
-FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
[value] using specification for function strlen
-FRAMAC_SHARE/libc/string.h:88:[value] Function strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:88:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
+FRAMAC_SHARE/libc/string.h:91:[value] Function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/string.h:90:[value] Function __e_acsl_strlen: postcondition got status unknown.
+FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown.
tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
--
GitLab