Skip to content
Snippets Groups Projects
Commit 76190d5c authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] oracles robusts against wp output

parent f3e0507e
No related branches found
No related tags found
No related merge requests found
...@@ -5,7 +5,6 @@ Now output intermediate result ...@@ -5,7 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Qed] Goal typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires : Valid [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_ZN1aE1c_call__ZN1a1bIvEEC1v_ZN1a1bIvEEC1v_requires : Valid
[wp] [Cache] not used
[wp] Proved goals: 2 / 2 [wp] Proved goals: 2 / 2
Qed: 2 Qed: 2
/* Generated by Frama-C */ /* Generated by Frama-C */
......
...@@ -5,7 +5,6 @@ Now output intermediate result ...@@ -5,7 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Qed] Goal typed_Z1m_assert_2 : Valid [wp] [Qed] Goal typed_Z1m_assert_2 : Valid
[wp] [Qed] Goal typed_Z1m_assert : Valid [wp] [Qed] Goal typed_Z1m_assert : Valid
[wp] [Cache] not used
[wp] Proved goals: 2 / 2 [wp] Proved goals: 2 / 2
Qed: 2 Qed: 2
/* Generated by Frama-C */ /* Generated by Frama-C */
......
...@@ -5,14 +5,13 @@ Now output intermediate result ...@@ -5,14 +5,13 @@ Now output intermediate result
[wp] 6 goals scheduled [wp] 6 goals scheduled
[wp] [Qed] Goal typed_Z1m_assert_4 : Valid [wp] [Qed] Goal typed_Z1m_assert_4 : Valid
[wp] [Qed] Goal typed_Z1m_assert_5 : 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_3 : Valid
[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid (4) [wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid (3) [wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid
[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid (6) [wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid
[wp] [Cache] updated:4
[wp] Proved goals: 6 / 6 [wp] Proved goals: 6 / 6
Qed: 2 Qed: 2
Alt-Ergo: 4 (6) Alt-Ergo: 4
/* Generated by Frama-C */ /* Generated by Frama-C */
static int i; static int i;
/*@ predicate pos(ℤ k) = k > 0; /*@ predicate pos(ℤ k) = k > 0;
......
...@@ -4,11 +4,10 @@ Now output intermediate result ...@@ -4,11 +4,10 @@ Now output intermediate result
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid [wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid
[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid (7) [wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid
[wp] [Cache] updated:1
[wp] Proved goals: 2 / 2 [wp] Proved goals: 2 / 2
Qed: 0 Qed: 0
Alt-Ergo: 2 (7) Alt-Ergo: 2
/* Generated by Frama-C */ /* Generated by Frama-C */
/*@ predicate positive(int i) = i > 0; /*@ predicate positive(int i) = i > 0;
*/ */
......
...@@ -5,7 +5,6 @@ Now output intermediate result ...@@ -5,7 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown [wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown
[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown [wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown
[wp] [Cache] updated:2
[wp] Proved goals: 0 / 2 [wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unknown: 2) Alt-Ergo: 0 (unknown: 2)
[wp] Warning: Memory model hypotheses for function '_Z1mPv': [wp] Warning: Memory model hypotheses for function '_Z1mPv':
......
...@@ -9,7 +9,6 @@ Now output intermediate result ...@@ -9,7 +9,6 @@ Now output intermediate result
[wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid [wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid [wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
[wp] [Qed] Goal typed_Z2m2_ensures : Valid [wp] [Qed] Goal typed_Z2m2_ensures : Valid
[wp] [Cache] not used
[wp] Proved goals: 3 / 3 [wp] Proved goals: 3 / 3
Qed: 3 Qed: 3
/* Generated by Frama-C */ /* Generated by Frama-C */
......
FILEREG:.*\.\(cc\|cpp\|ii\)$ 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" 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/' FILTER:/bin/sed -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e 's/Alt-Ergo [0-9.]\+/Alt-Ergo/'
...@@ -5,6 +5,5 @@ Now output intermediate result ...@@ -5,6 +5,5 @@ Now output intermediate result
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid [wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid
[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures : Valid [wp] [Qed] Goal typed_ZN6Point2E3foo_ensures : Valid
[wp] [Cache] not used
[wp] Proved goals: 2 / 2 [wp] Proved goals: 2 / 2
Qed: 2 Qed: 2
/* run.config /* 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 class Point2
{ {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment