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

[tests] update oracles

parent 51dd8503
No related branches found
No related tags found
No related merge requests found
......@@ -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;
......
......@@ -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;
*/
......
......@@ -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);
......
# frama-c -wp [...]
[kernel] Parsing tests/specs/wp_empty_struct.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
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