Skip to content
Snippets Groups Projects
Commit 0f9cfa83 authored by Allan Blanchard's avatar Allan Blanchard Committed by Virgile Prevosto
Browse files

Robustify WP tests

parent d494d7d8
No related branches found
No related tags found
No related merge requests found
......@@ -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 */
......
......@@ -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 */
......
......@@ -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
......
......@@ -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:
......
......@@ -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 */
......
......@@ -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
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"
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