diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle index 4aea35528b7fd3009e061b7f14020eb92c1f7e8b..ad84c99eb9025f3fed969dd44d4af5eafd6b693b 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 fe474be8bfa4f1c87a677020433294cab84ce90a..8d7efd4fd7dffe99612c6917c8c342a025639e1d 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 8ea826cb0780c57de410a3a1bf55a6b737398b40..cd2c02e3c50f4a93ee92689f59717d378eaf447c 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 1ab770b4e10ae6d150288a42a89d5f498c746a69..c9eca49891c6aa386d60b9431224e5978bba1829 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 565d61b3af0619633e4dc232fb1569e3b3d4261d..a89011312ffab6b7a4b2cc2e92132cf008c533d0 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 4c75afb853de8203fc3b6052579d3475cd22d6b1..a3d27a6d1e75ae51b2de8892a0a42eaf111d94cd 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 db022e84f4c58666aa66f0cadd6c8fa60718008d..28633d29c79de8b865d6d57bb4d4ff4d33af3f2a 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 1bb44f5331b1cf57217fc927509b0ae3a4255f93..43a2493d9748c6e2f4cf3df84b6fcb8c981f7e08 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 6bddcc0b2d0df53f00f3097ab8948ddff858a9a9..69db388327b82bd4be7b8762ba6e32eb5d72576c 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 {