From 7ab6557c74d2d08316a92c48e31e9a15ff0a2c1b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 19 Feb 2021 16:11:11 +0100
Subject: [PATCH] [Eva] Updates test oracles.
---
.../tests/arith/oracle_ci/quantif.res.oracle | 1 -
tests/builtins/oracle/strchr.res.oracle | 2 ++
tests/libc/oracle/stdlib_c_env.res.oracle | 2 ++
tests/libc/oracle/string_c.res.oracle | 2 ++
tests/libc/oracle/string_c_generic.res.oracle | 2 ++
tests/libc/oracle/string_c_strchr.res.oracle | 2 ++
tests/libc/oracle/string_h.res.oracle | 14 ++++----------
tests/value/oracle/annot_valid.res.oracle | 2 +-
8 files changed, 15 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
index 046a6a7f967..888e5f6719e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
@@ -3,7 +3,6 @@
[eva:alarm] tests/arith/quantif.i:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/quantif.i:15: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:20: Warning: assertion got status unknown.
[eva:alarm] tests/arith/quantif.i:24: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown.
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index 21fd920919a..770361f5470 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -23,6 +23,8 @@
[eva] tests/builtins/strchr.c:88: Call to builtin strchr
[eva] tests/builtins/strchr.c:88:
function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva] tests/builtins/strchr.c:88: Frama_C_show_each_mystrchr: {3}
[eva] tests/builtins/strchr.c:89: assertion got status valid.
[eva] tests/builtins/strchr.c:92: Call to builtin strchr
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index fc9107a8102..e39d01ba5bf 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -9,6 +9,8 @@
[eva] share/libc/stdlib.c:114: Call to builtin strchr
[eva] share/libc/stdlib.c:114:
function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva] share/libc/stdlib.c:115:
assertion 'string_contains_separator' got status valid.
[eva] share/libc/stdlib.c:116: assertion 'name_is_not_empty' got status valid.
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 033c83c6b47..401829973b4 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -668,6 +668,8 @@
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva:alarm] share/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] share/libc/string.h:171:
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index d2f546a60ac..4e1e5145535 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -288,6 +288,8 @@
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva:alarm] share/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] share/libc/string.h:171:
diff --git a/tests/libc/oracle/string_c_strchr.res.oracle b/tests/libc/oracle/string_c_strchr.res.oracle
index 965af4a3862..d389a3cf561 100644
--- a/tests/libc/oracle/string_c_strchr.res.oracle
+++ b/tests/libc/oracle/string_c_strchr.res.oracle
@@ -67,6 +67,8 @@
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva:alarm] share/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] Recording results for strchr
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 5e1e94a0719..fd2eaee19bf 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -143,12 +143,8 @@
[eva] tests/libc/string_h.c:75:
function strtok: precondition 'valid_string_delim' got status valid.
[eva:alarm] tests/libc/string_h.c:75: Warning:
- function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:75:
- Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+ function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
[eva] Done for function strtok
-[eva:alarm] tests/libc/string_h.c:76: Warning:
- assertion 'unreachable_if_precise' got status invalid (stopping propagation).
[eva] Recording results for test_strtok
[eva] Done for function test_strtok
[eva] computing for function test_strtok_r <- main.
@@ -232,12 +228,8 @@
[eva] tests/libc/string_h.c:105:
function strtok_r: precondition 'valid_saveptr' got status valid.
[eva:alarm] tests/libc/string_h.c:105: Warning:
- function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:105:
- Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+ function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
[eva] Done for function strtok_r
-[eva:alarm] tests/libc/string_h.c:106: Warning:
- assertion 'unreachable_if_precise' got status invalid (stopping propagation).
[eva] Recording results for test_strtok_r
[eva] Done for function test_strtok_r
[eva] computing for function strdup <- main.
@@ -333,6 +325,8 @@
[eva] tests/libc/string_h.c:154: Call to builtin strchr
[eva] tests/libc/string_h.c:154:
function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva] computing for function strchrnul <- main.
Called from tests/libc/string_h.c:155.
[eva] using specification for function strchrnul
diff --git a/tests/value/oracle/annot_valid.res.oracle b/tests/value/oracle/annot_valid.res.oracle
index 88f57174bb9..557e8ca2b58 100644
--- a/tests/value/oracle/annot_valid.res.oracle
+++ b/tests/value/oracle/annot_valid.res.oracle
@@ -17,7 +17,7 @@
[eva:alarm] tests/value/annot_valid.i:29: Warning: assertion got status unknown.
[eva:alarm] tests/value/annot_valid.i:32: Warning: assertion got status unknown.
[eva:alarm] tests/value/annot_valid.i:35: Warning: assertion got status unknown.
-[eva:alarm] tests/value/annot_valid.i:38: Warning: assertion got status unknown.
+[eva] tests/value/annot_valid.i:38: assertion got status valid.
[eva] tests/value/annot_valid.i:41: assertion got status valid.
[eva:alarm] tests/value/annot_valid.i:44: Warning:
assertion got status invalid (stopping propagation).
--
GitLab