Commit 06ff8189 authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] add « Unsuccess » line in shell mode

parent ff6d0d73
......@@ -390,7 +390,12 @@ let do_report_scheduled () =
)
) gstats.provers ;
if gstats.failed > 0 then add_line "Failed" gstats.failed none ;
if not shell then
if shell then
begin
let n = gstats.timeout + gstats.unknown in
if n > 0 then add_line "Unsuccess" n none
end
else
begin
if gstats.timeout > 0 then add_line "Timeout" gstats.timeout none ;
if gstats.unknown > 0 then add_line "Unknown" gstats.unknown none ;
......
......@@ -9,6 +9,7 @@
[wp] 1 goal scheduled
[wp] [Unsuccess] typed_foo_assert_MUST_FAIL (Alt-Ergo) (Cached) (Stronger)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 1 0.0%
......
......@@ -7,6 +7,7 @@
[wp] 1 goal scheduled
[wp] [Unsuccess] typed_automaton_state_accessor_assert (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
automaton_state_accessor - - 1 0.0%
......
......@@ -8,6 +8,7 @@
[wp] [Unsuccess] typed_foo_ensures (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_foo_exits (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 2
Unsuccess: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 2 0.0%
......
......@@ -39,6 +39,7 @@
[wp] Proved goals: 19 / 27
Qed: 18
Alt-Ergo: 1
Unsuccess: 8
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
empty 1 - 1 100%
......
......@@ -27,6 +27,7 @@
[wp] Proved goals: 15 / 19
Qed: 13
Alt-Ergo: 2
Unsuccess: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 5 - 5 100%
......
......@@ -9,6 +9,7 @@
[wp] [Unsuccess] typed_min_bx_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_min_by_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 5
Unsuccess: 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f - - 3 0.0%
......
......@@ -10,6 +10,7 @@
[wp] [Valid] hoare_bts0513_bis_assert_qed_ok_ok (Qed)
[wp] Proved goals: 1 / 4
Qed: 1
Unsuccess: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
bts0513 - - 2 0.0%
......
......@@ -5,6 +5,7 @@
[wp] 1 goal scheduled
[wp] [Unsuccess] typed_cast_sgn_usgn_ensures_qed_ko_KO (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
cast_sgn_usgn - - 1 0.0%
......
......@@ -48,6 +48,7 @@
[wp] Proved goals: 33 / 42
Qed: 29
Alt-Ergo: 4
Unsuccess: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 4 2 6 100%
......
......@@ -32,6 +32,7 @@
[wp] Proved goals: 22 / 26
Qed: 15
Alt-Ergo: 7
Unsuccess: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
......
......@@ -14,6 +14,7 @@
[wp] [Valid] typed_assigned_glob_array_check_OK (Alt-Ergo) (Cached)
[wp] Proved goals: 2 / 9
Alt-Ergo: 2
Unsuccess: 7
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
atomic - - 1 0.0%
......
......@@ -7,6 +7,7 @@
[wp] [Unsuccess] typed_comp_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_array_check_FAIL (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 3
Unsuccess: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
atomic - - 1 0.0%
......
......@@ -10,6 +10,7 @@
[wp] [Unsuccess] typed_call_assigns_t4_assigns_exit (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_call_assigns_t4_assigns_normal (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 6
Unsuccess: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
call_assigns_t1 - - 2 0.0%
......
......@@ -16,6 +16,7 @@
[wp] Proved goals: 8 / 10
Qed: 3
Alt-Ergo: 5
Unsuccess: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 3 5 10 80.0%
......
......@@ -11,6 +11,7 @@
[wp] Proved goals: 3 / 5
Qed: 2
Alt-Ergo: 1
Unsuccess: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 2 1 3 100%
......
......@@ -10,6 +10,7 @@
[wp] [Unsuccess] typed_lxor_check_A (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_lxor_check_B (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 6
Unsuccess: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
land - - 2 0.0%
......
......@@ -9,6 +9,7 @@
[wp] [Valid] typed_main_assert_a2 (Qed)
[wp] Proved goals: 2 / 4
Qed: 2
Unsuccess: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
main 2 - 4 50.0%
......
......@@ -9,6 +9,7 @@
[wp] [Valid] typed_usable_lemma_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 2 / 3
Alt-Ergo: 2
Unsuccess: 1
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 1 0.0%
......
......@@ -47,6 +47,7 @@
Terminating: 1
Qed: 9
Alt-Ergo: 1
Unsuccess: 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
simpl_r 1 1 2 100%
......
Supports Markdown
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