diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle index cd2c02e3c50f4a93ee92689f59717d378eaf447c..bc36bc2635df80ad79d5fd089a772a1bd319c740 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 c9eca49891c6aa386d60b9431224e5978bba1829..9947e135d7bb41de300eea5d4da858c2599c2d33 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 93fad4096b8411cc0ee568313f9a1a9a92fadf2a..af2e9c07c7293c4dedfe45d9f06a9ff56bdae71d 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 43a2493d9748c6e2f4cf3df84b6fcb8c981f7e08..cc31f6145aa801e25eb33b1d9ceedecc509d3f98 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...