Commit f335209f authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/wp/terminates-result-display' into 'master'

WP displays trivial terminates proofs

See merge request frama-c/frama-clang!150
parents 0d573024 02791eaa
......@@ -3,11 +3,16 @@
Now output intermediate result
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] [CFG] Goal Z2m2_terminates : Valid (Trivial)
[wp] [CFG] Goal Z2m3_terminates : Valid (Trivial)
[wp] [CFG] Goal Z2m4_terminates : Valid (Trivial)
[wp] [CFG] Goal Z3m3a_terminates : Valid (Trivial)
[wp] [CFG] Goal Z3m3b_terminates : Valid (Trivial)
[wp] 3 goals scheduled
[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
[wp] Proved goals: 8 / 8
Qed: 3
/* Generated by Frama-C */
/*@ behavior c:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment