diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle index 5329ef6f11cf2c4bd3158cd0235eb03306f5d817..11f9b2e61d9891c66e6b9c6506dbe7c54f4112e5 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 95a1a4e393e1afac010b4e760534fc926e5ea1b2..4648dadf04088fda5cbde5edf8fd672077dcb197 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 55fffbb874fe693f31443e5643dc55434b52d718..e57bc1c06cb330c67efe190a99b6902d9e7b3f9b 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 b3163d1b5938d421aef592e40612211283e07a6b..fba2a737f9577e701f747eb5ce404319c10ba7d8 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 8e5f08430c384e6594b5add5050f563405641c2e..9b5a7ccd075f8933eb54a906db21a5ab0e1af3ff 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 cc31f6145aa801e25eb33b1d9ceedecc509d3f98..a55613cb57838155d41f73ec00948a3bfc260ab7 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 72b8655548bc640c60e77831da4b8b93bd683b55..bca199dd56d3ddaaadcd6d58684eeb1853782f6b 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"