From 1e3d8db32a9ec702822095fabf48ec925e96111d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 7 Oct 2020 12:26:24 +0200
Subject: [PATCH] Robustify WP tests

---
 tests/bugs/oracle/issue11.res.oracle          | 2 +-
 tests/bugs/oracle/issue23.res.oracle          | 2 +-
 tests/bugs/oracle/issue24.res.oracle          | 6 +++---
 tests/bugs/oracle/logiccast.res.oracle        | 2 +-
 tests/bugs/oracle/term.res.oracle             | 4 ++--
 tests/specs/oracle/wp_empty_struct.res.oracle | 2 +-
 tests/test_config                             | 2 +-
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index 5329ef6f..11f9b2e6 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -4,8 +4,8 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [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] [Qed] Goal typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires : Valid
 [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 95a1a4e3..4648dadf 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -4,8 +4,8 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_Z1m_assert_2 : Valid
 [wp] [Qed] Goal typed_Z1m_assert : Valid
+[wp] [Qed] Goal typed_Z1m_assert_2 : Valid
 [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 55fffbb8..e57bc1c0 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -4,11 +4,11 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
+[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid
 [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] Proved goals:    6 / 6
   Qed:             2 
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index b3163d1b..fba2a737 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -4,8 +4,8 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unsuccess
 [wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unsuccess
+[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unsuccess
 [wp] Proved goals:    0 / 2
   Alt-Ergo:        0  (unsuccess: 2)
 [wp] tests/bugs/logiccast.cpp:3: Warning: 
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index 8e5f0843..9b5a7ccd 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -7,9 +7,9 @@ Now output intermediate result
    \true
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
-[wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
-[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
 [wp] [Qed] Goal typed_Z2m2_ensures : Valid
+[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
+[wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
 [wp] Proved goals:    3 / 3
   Qed:             3
 /* Generated by Frama-C */
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index cc31f614..a55613cb 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -4,7 +4,7 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid
 [wp] [Qed] Goal typed_ZN6Point2E3foo_ensures : Valid
+[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid
 [wp] Proved goals:    2 / 2
   Qed:             2
diff --git a/tests/test_config b/tests/test_config
index 72b86555..bca199dd 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,6 +1,6 @@
 FILEREG:.*\.\(cc\|cpp\|ii\)$
 MACRO: CXX -cxx-c++stdlib-path share/libc++ -cxx-clang-command="bin/framaCIRGen"
 MACRO: EVA -eva -eva-msg-key=-summary
-MACRO: WP -wp -wp-session tests/wp-cache -wp-cache update -wp-msg-key shell
+MACRO: WP -wp -wp-par 1 -wp-session tests/wp-cache -wp-cache update -wp-msg-key shell
 OPT:-print -check @CXX@
 FILTER:/bin/sed  -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|$(pwd)/||g"
-- 
GitLab