From 475a0e01447216de967ec319691a6b4edd5c00a7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 5 Aug 2020 16:40:56 +0200
Subject: [PATCH] [tests] update oracles

---
 tests/bugs/oracle/issue24.res.oracle          | 12 ++++++------
 tests/bugs/oracle/issue27-pred.res.oracle     |  6 +++---
 tests/bugs/oracle/logiccast.res.oracle        |  6 +++---
 tests/specs/oracle/wp_empty_struct.res.oracle |  1 +
 4 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index cd2c02e3..bc36bc26 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -5,13 +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
-[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] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid (unqualified)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid (unqualified)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid (unqualified)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid (unqualified)
 [wp] Proved goals:    6 / 6
-  Qed:               2 
-  Alt-Ergo:    4
+  Qed:             2 
+  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 c9eca498..9947e135 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -4,10 +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
+[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid (unqualified)
 [wp] Proved goals:    2 / 2
-  Qed:               0 
-  Alt-Ergo:    2
+  Qed:             0 
+  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 93fad409..af2e9c07 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -3,10 +3,10 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Timeout
-[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Timeout
+[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unsuccess
+[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unsuccess
 [wp] Proved goals:    0 / 2
-  Alt-Ergo:    0  (interrupted: 2)
+  Alt-Ergo:        0  (unsuccess: 2)
 [wp] Warning: Memory model hypotheses for function '_Z1mPv':
   /*@ behavior typed: requires \separated(&base,r+(..)); */
   void _Z1mPv(void *r);
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index 43a2493d..cc31f614 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
 [kernel] Parsing tests/specs/wp_empty_struct.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
-- 
GitLab