From 76190d5ccf5195b804d7b02a49f7be6d9fbbad4e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 2 Dec 2019 16:54:07 +0100
Subject: [PATCH] [tests] oracles robusts against wp output
---
tests/bugs/oracle/issue11.res.oracle | 1 -
tests/bugs/oracle/issue23.res.oracle | 1 -
tests/bugs/oracle/issue24.res.oracle | 11 +++++------
tests/bugs/oracle/issue27-pred.res.oracle | 5 ++---
tests/bugs/oracle/logiccast.res.oracle | 1 -
tests/bugs/oracle/term.res.oracle | 1 -
tests/bugs/test_config | 2 +-
tests/specs/oracle/wp_empty_struct.res.oracle | 1 -
tests/specs/wp_empty_struct.cpp | 2 +-
9 files changed, 9 insertions(+), 16 deletions(-)
diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index 4aea3552..ad84c99e 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -5,7 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Qed] Goal typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires : Valid
[wp] [Qed] Goal typed___fc_init_ZN1aE1c_call__ZN1a1bIvEEC1v_ZN1a1bIvEEC1v_requires : Valid
-[wp] [Cache] not used
[wp] Proved goals: 2 / 2
Qed: 2
/* Generated by Frama-C */
diff --git a/tests/bugs/oracle/issue23.res.oracle b/tests/bugs/oracle/issue23.res.oracle
index fe474be8..8d7efd4f 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -5,7 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_Z1m_assert_2 : Valid
[wp] [Qed] Goal typed_Z1m_assert : Valid
-[wp] [Cache] not used
[wp] Proved goals: 2 / 2
Qed: 2
/* Generated by Frama-C */
diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index 8ea826cb..cd2c02e3 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -5,14 +5,13 @@ Now output intermediate result
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_Z1m_assert_4 : Valid
[wp] [Qed] Goal typed_Z1m_assert_5 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid (5)
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid (4)
-[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid (3)
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid (6)
-[wp] [Cache] updated:4
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid
[wp] Proved goals: 6 / 6
Qed: 2
- Alt-Ergo: 4 (6)
+ Alt-Ergo: 4
/* Generated by Frama-C */
static int i;
/*@ predicate pos(ℤ k) = k > 0;
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index 1ab770b4..c9eca498 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -4,11 +4,10 @@ Now output intermediate result
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid (7)
-[wp] [Cache] updated:1
+[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid
[wp] Proved goals: 2 / 2
Qed: 0
- Alt-Ergo: 2 (7)
+ Alt-Ergo: 2
/* Generated by Frama-C */
/*@ predicate positive(int i) = i > 0;
*/
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index 565d61b3..a8901131 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -5,7 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown
[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown
-[wp] [Cache] updated:2
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unknown: 2)
[wp] Warning: Memory model hypotheses for function '_Z1mPv':
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index 4c75afb8..a3d27a6d 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -9,7 +9,6 @@ Now output intermediate result
[wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
[wp] [Qed] Goal typed_Z2m2_ensures : Valid
-[wp] [Cache] not used
[wp] Proved goals: 3 / 3
Qed: 3
/* Generated by Frama-C */
diff --git a/tests/bugs/test_config b/tests/bugs/test_config
index db022e84..28633d29 100644
--- a/tests/bugs/test_config
+++ b/tests/bugs/test_config
@@ -1,4 +1,4 @@
FILEREG:.*\.\(cc\|cpp\|ii\)$
MACRO: CXX -machdep=x86_64 -cxx-c++stdlib-path share/libc++ -cxx-clang-command="bin/framaCIRGen -target x86_64-linux-gnu -D__FC_MACHDEP_X86_64"
-OPT:-print -wp -wp-msg-key no-time-info @CXX@
+OPT:-print -wp -wp-msg-key="no-time-info,no-step-info" -wp-cache none @CXX@
FILTER:/bin/sed -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e 's/Alt-Ergo [0-9.]\+/Alt-Ergo/'
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index 1bb44f53..43a2493d 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -5,6 +5,5 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid
[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures : Valid
-[wp] [Cache] not used
[wp] Proved goals: 2 / 2
Qed: 2
diff --git a/tests/specs/wp_empty_struct.cpp b/tests/specs/wp_empty_struct.cpp
index 6bddcc0b..69db3883 100644
--- a/tests/specs/wp_empty_struct.cpp
+++ b/tests/specs/wp_empty_struct.cpp
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp -wp-msg-key="no-time-info,no-step-info" @CXX@
+OPT: -wp -wp-msg-key="no-time-info,no-step-info" -wp-cache none @CXX@
*/
class Point2
{
--
GitLab