Skip to content
Snippets Groups Projects
Commit 5cfa60c8 authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] update test

parent c1701ced
No related branches found
No related tags found
No related merge requests found
......@@ -16,7 +16,7 @@
axiom loop3: \forall integer n; R(n) ==> P(n+1);
}*/
//@ terminates \false;
int foo(int x)
{
int n = 0;
......
......@@ -7,7 +7,7 @@
[wp] [Passed] (Unsuccess) typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] [Passed] (Unsuccess) typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Passed] (Unsuccess) typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_foo_terminates (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_terminates (Qed)
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_B_preserved (Alt-Ergo) (Cached)
......@@ -15,18 +15,17 @@
[wp] [Valid] typed_foo_loop_invariant_C_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_C_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_assigns (Qed)
[wp] Proved goals: 11 / 12
[wp] Proved goals: 12 / 12
Unreachable: 1
Qed: 1
Qed: 2
Alt-Ergo: 9
Unsuccess: 1
Smoke Tests: 3 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo 1 9 11 90.9%
foo 2 9 11 100%
------------------------------------------------------------
Qed Ergo Failed
foo_terminates - - 1
foo_terminates 1 - -
foo_loop_assigns 1 - -
foo_loop_invariant_A - 2 -
foo_loop_invariant_B - 2 -
......@@ -35,8 +34,8 @@
foo_wp_smoke_dead_code_s9 - 1 -
foo_wp_smoke_dead_loop_s2 - 1 -
-------------------------------------------------------------
Success: 87.5%
Success: 100%
Total : 8 properties
Valid : 7
Failed : 1
Valid : 8
Failed : -
-------------------------------------------------------------
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