Commit 033480b5 authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] update tests oracles with new printing

parent fb5c6303
......@@ -219,7 +219,8 @@ let pp_stats ~shell ~updating fmt s =
Format.fprintf fmt ")"
) s.provers ;
if 0 < s.cached then
if 0 < s.cached && List.exists (fun (p,_) -> p <> Qed) s.provers
if s.cached = vp || updating then
Format.fprintf fmt " (Cached)"
......@@ -202,10 +202,12 @@ type result = {
prover_errmsg : string ;
let is_verdict r = match r.verdict with
let is_result = function
| Valid | Unknown | Invalid | Timeout | Stepout | Failed -> true
| NoResult | Computing _ -> false
let is_verdict r = is_result r.verdict
let is_valid = function { verdict = Valid } -> true | _ -> false
let is_computing = function { verdict=Computing _ } -> true | _ -> false
......@@ -111,6 +111,7 @@ val cached : result -> result (** only for true verdicts *)
val result : ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
val is_auto : prover -> bool
val is_result : verdict -> bool
val is_verdict : result -> bool
val is_valid: result -> bool
val is_computing: result -> bool
......@@ -295,56 +295,14 @@ let do_wpo_result goal prover res =
do_wpo_stat goal prover res ;
let results g =
(fun (_,r) -> VCS.is_verdict r)
(Wpo.get_results g)
let do_wpo_failed goal =
let updating = Cache.is_updating () in
match results goal with
| [p,r] ->
Wp_parameters.result "[%a] Goal %s : %t%a"
VCS.pp_prover p (Wpo.get_gid goal)
(VCS.pp_result_qualif ~updating p r) pp_warnings goal
| pres ->
Wp_parameters.result "[Failed] Goal %s%t" (Wpo.get_gid goal)
begin fun fmt ->
pp_warnings fmt goal ;
(fun (p,r) ->
Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
(VCS.title_of_prover p)
(VCS.pp_result_qualif ~updating p r)
) pres ;
let do_wpo_smoke status goal =
Wp_parameters.result "[%s] Smoke-test %s%t"
(match status with
| `Failed -> "Failed"
| `Passed -> "Passed"
| `Unknown -> "Partial")
(Wpo.get_gid goal)
begin fun fmt ->
pp_warnings fmt goal ;
let updating = Cache.is_updating () in
(fun (p,r) ->
Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
(VCS.title_of_prover p)
(VCS.pp_result_qualif ~updating p r)
) (results goal) ;
[@@@ warning "-32"]
let do_report_stats ~shell ~updating ~smoke goal (verdict,stats) =
let status =
if smoke then
match verdict with
| VCS.NoResult | Computing _ -> ""
| Invalid -> "Passed"
| Valid -> "Failed"
| Valid -> "Failed (Doomed)"
| Failed -> "Unknown (Failure)"
| Invalid -> "Passed (Invalid)"
| Unknown -> "Passed (Unknown)"
| Timeout -> "Passed (Timeout)"
| Stepout -> "Passed (Stepout)"
......@@ -361,7 +319,6 @@ let do_report_stats ~shell ~updating ~smoke goal (verdict,stats) = "[%s] %s%a%a"
status (Wpo.get_gid goal) (Stats.pp_stats ~shell ~updating) stats
pp_warnings goal
[@@@ warning "+32"]
let do_wpo_success ~shell ~updating goal success =
if Wp_parameters.Generate.get () then
......@@ -371,32 +328,18 @@ let do_wpo_success ~shell ~updating goal success = ~ontty:`Silent
"[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
if Wpo.is_smoke_test goal then
begin match success with
| None -> ~ontty:`Silent
"[Passed] Smoke-test %s" (Wpo.get_gid goal)
| Some _ ->
let status,target = Wpo.get_proof goal in
do_wpo_smoke status goal ;
if status = `Failed then
let smoke = Wpo.is_smoke_test goal in
let prs = Wpo.get_results goal in
let (verdict,_) as vstats = Stats.results ~smoke prs in
if shell || verdict <> Valid then
do_report_stats ~shell ~updating goal ~smoke vstats ;
if smoke && verdict <> Valid then
let target = Wpo.get_target goal in
let source = fst (Property.location target) in
Wp_parameters.warning ~source "Failed smoke-test"
begin match success with
| None -> do_wpo_failed goal
| Some (VCS.Tactical as script) -> ~ontty:`Silent
"[%a] Goal %s : Valid"
VCS.pp_prover script (Wpo.get_gid goal)
| Some prover ->
ignore shell ;
let result = Wpo.get_result goal prover in ~ontty:`Silent
"[%a] Goal %s : %t"
VCS.pp_prover prover (Wpo.get_gid goal)
(VCS.pp_result_qualif ~updating prover result)
end ;
let do_report_time fmt s =
......@@ -7,7 +7,7 @@
[wp] bad_cast_call.i:8: Warning:
Cast with incompatible pointers types (source: sint8*) (target: char**)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_MUST_FAIL : Unsuccess (Stronger)
[wp] [Unknown] typed_foo_assert_MUST_FAIL (Alt-Ergo) (Cached) (Stronger)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
......@@ -3,21 +3,21 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part1 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part2 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part3 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_established : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_preserved_part1 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_preserved_part2 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_preserved_part3 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_established : Valid
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_loop_continue_loop_invariant_established : Valid
[wp] [Qed] Goal typed_loop_continue_loop_assigns : Valid
[wp] [Valid] typed_loop_switch_loop_invariant_preserved_part1 (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_preserved_part2 (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_preserved_part3 (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_established (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_2_preserved_part1 (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_2_preserved_part2 (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_2_preserved_part3 (Qed)
[wp] [Valid] typed_loop_switch_loop_invariant_2_established (Qed)
[wp] [Valid] typed_loop_switch_loop_assigns_part1 (Qed)
[wp] [Valid] typed_loop_switch_loop_assigns_part2 (Qed)
[wp] [Valid] typed_loop_switch_loop_assigns_part3 (Qed)
[wp] [Valid] typed_loop_switch_loop_assigns_part4 (Qed)
[wp] [Valid] typed_loop_continue_loop_invariant_preserved (Qed)
[wp] [Valid] typed_loop_continue_loop_invariant_established (Qed)
[wp] [Valid] typed_loop_continue_loop_assigns (Qed)
[wp] Proved goals: 15 / 15
Qed: 15
......@@ -5,7 +5,7 @@
[wp] default-stmt-assigns.i:2: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_automaton_state_accessor_assert : Unsuccess
[wp] [Unknown] typed_automaton_state_accessor_assert (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
......@@ -5,8 +5,8 @@
Neither code nor specification for function bar, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_ensures : Unsuccess
[wp] [Alt-Ergo] Goal typed_foo_exits : Unsuccess
[wp] [Unknown] typed_foo_ensures (Alt-Ergo) (Cached)
[wp] [Unknown] typed_foo_exits (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unsuccess: 2)
......@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
[wp] [Valid] typed_f_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo: 1
......@@ -9,33 +9,33 @@
[wp] stmtcompiler_test.i:81: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 27 goals scheduled
[wp] [Qed] Goal typed_empty_assert : Valid
[wp] [Qed] Goal typed_one_assign_assert : Valid
[wp] [Qed] Goal typed_one_if_assert : Valid
[wp] [Qed] Goal typed_some_seq_assert : Valid
[wp] [Qed] Goal typed_some_seq_assert_2 : Valid
[wp] [Qed] Goal typed_main_ensures_result_assert : Valid
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unsuccess
[wp] [Qed] Goal typed_main_assigns_global_assert : Valid
[wp] [Qed] Goal typed_main_assigns_global_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unsuccess
[wp] [Qed] Goal typed_zloop_ensures : Valid
[wp] [Alt-Ergo] Goal typed_zloop_loop_invariant_preserved : Unsuccess
[wp] [Qed] Goal typed_zloop_loop_invariant_established : Valid
[wp] [Qed] Goal typed_zloop_assert : Valid
[wp] [Qed] Goal typed_zloop_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_zloop_assert_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_zloop_assert_bad : Unsuccess
[wp] [Qed] Goal typed_behavior2_assert : Valid
[wp] [Qed] Goal typed_behavior3_assert : Valid
[wp] [Qed] Goal typed_behavior4_assert : Valid
[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unsuccess
[wp] [Alt-Ergo] Goal typed_if_assert_assert : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unsuccess
[wp] [Qed] Goal typed_if_assert_assert_3 : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unsuccess
[wp] [Qed] Goal typed_compare_assert : Valid
[wp] [Valid] typed_empty_assert (Qed)
[wp] [Valid] typed_one_assign_assert (Qed)
[wp] [Valid] typed_one_if_assert (Qed)
[wp] [Valid] typed_some_seq_assert (Qed)
[wp] [Valid] typed_some_seq_assert_2 (Qed)
[wp] [Valid] typed_main_ensures_result_assert (Qed)
[wp] [Valid] typed_main_assert (Qed)
[wp] [Timeout] typed_not_main_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assigns_global_assert (Qed)
[wp] [Valid] typed_main_assigns_global_assert_2 (Qed)
[wp] [Timeout] typed_main_assigns_global_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_zloop_ensures (Qed)
[wp] [Timeout] typed_zloop_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_zloop_loop_invariant_established (Qed)
[wp] [Valid] typed_zloop_assert (Qed)
[wp] [Valid] typed_zloop_assert_2 (Qed)
[wp] [Timeout] typed_zloop_assert_3 (Alt-Ergo) (Cached)
[wp] [Timeout] typed_zloop_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_behavior2_assert (Qed)
[wp] [Valid] typed_behavior3_assert (Qed)
[wp] [Valid] typed_behavior4_assert (Qed)
[wp] [Unknown] typed_behavior5_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_if_assert_assert (Alt-Ergo) (Cached)
[wp] [Timeout] typed_if_assert_assert_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_if_assert_assert_3 (Qed)
[wp] [Timeout] typed_if_assert_assert_missing_return (Alt-Ergo) (Cached)
[wp] [Valid] typed_compare_assert (Qed)
[wp] Proved goals: 19 / 27
Qed: 18
Alt-Ergo: 1 (unsuccess: 8)
......@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_empty_assert : Valid
[wp] [Valid] typed_empty_assert (Qed)
[wp] Proved goals: 1 / 1
Qed: 1
......@@ -5,25 +5,25 @@
[wp] wp_behav.c:82: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 19 goals scheduled
[wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_x1_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_assert_qed_ok : Valid
[wp] [Qed] Goal typed_f_x2_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_assert_qed_ok_2 : Valid
[wp] [Qed] Goal typed_min_complete_bx_by : Valid
[wp] [Qed] Goal typed_min_disjoint_bx_by : Valid
[wp] [Qed] Goal typed_min_bx_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_min_by_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_bhv_complete_neg_pos : Valid
[wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unsuccess
[wp] [Qed] Goal typed_assert_needed_assert_qed_ok_ok_with_hyp : Valid
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_razT_loop_invariant_qed_ok_preserved : Valid
[wp] [Qed] Goal typed_razT_loop_invariant_qed_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unsuccess
[wp] [Valid] typed_f_ensures_qed_ok (Qed)
[wp] [Valid] typed_f_x1_ensures_qed_ok (Qed)
[wp] [Valid] typed_f_assert_qed_ok (Qed)
[wp] [Valid] typed_f_x2_ensures_qed_ok (Qed)
[wp] [Valid] typed_f_assert_qed_ok_2 (Qed)
[wp] [Valid] typed_min_complete_bx_by (Qed)
[wp] [Valid] typed_min_disjoint_bx_by (Qed)
[wp] [Valid] typed_min_bx_ensures_qed_ok (Qed)
[wp] [Valid] typed_min_by_ensures_qed_ok (Qed)
[wp] [Valid] typed_bhv_complete_neg_pos (Alt-Ergo) (Cached)
[wp] [Valid] typed_bhv_pos_ensures_qed_ok (Qed)
[wp] [Valid] typed_bhv_neg_ensures_qed_ok (Qed)
[wp] [Timeout] typed_assert_needed_assert_ko (Alt-Ergo) (Cached)
[wp] [Valid] typed_assert_needed_assert_qed_ok_ok_with_hyp (Qed)
[wp] [Unknown] typed_bts0513_ensures_ko1 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_bts0513_ensures_ko2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_razT_loop_invariant_qed_ok_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_razT_loop_invariant_qed_ok_established (Qed)
[wp] [Timeout] typed_razT_b1_ensures_e1 (Alt-Ergo) (Cached)
[wp] Proved goals: 15 / 19
Qed: 13
Alt-Ergo: 2 (unsuccess: 4)
......@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_x1_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_x2_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_min_bx_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_min_by_ensures_qed_ko : Unsuccess
[wp] [Stepout] typed_f_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unknown] typed_f_x1_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unknown] typed_f_x2_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Stepout] typed_min_bx_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Timeout] typed_min_by_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 5
Alt-Ergo: 0 (unsuccess: 5)
......@@ -7,15 +7,15 @@
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
[wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_call_g_call_g_requires_qed_ok_Rga : Valid
[wp] [Qed] Goal typed_call_g_call_g_requires_Rgb : Valid
[wp] [Valid] typed_double_call_call_f_requires_qed_ok_Rf (Qed)
[wp] [Valid] typed_double_call_call_f_2_requires_qed_ok_Rf (Qed)
[wp] [Valid] typed_main_requires_qed_ok_Rmain (Qed)
[wp] [Valid] typed_main_ensures_qed_ok_Emain (Qed)
[wp] [Valid] typed_main_call_f_requires_qed_ok_Rf (Qed)
[wp] [Valid] typed_call_main_ensures_qed_ok (Qed)
[wp] [Valid] typed_call_main_call_main_requires_qed_ok_Rmain (Qed)
[wp] [Valid] typed_call_g_call_g_requires_qed_ok_Rga (Qed)
[wp] [Valid] typed_call_g_call_g_requires_Rgb (Qed)
[wp] Proved goals: 9 / 9
Qed: 9
......@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
[wp] [Valid] typed_f_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo: 1
......@@ -4,10 +4,10 @@
[rte:annot] annotating function bts0513_bis
[wp] Running WP plugin...
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_bis_assert_qed_ko_ko1 : Unsuccess
[wp] [Qed] Goal hoare_bts0513_bis_assert_qed_ok_ok : Valid
[wp] [Unknown] hoare_bts0513_ensures_qed_ko_ko1 (Alt-Ergo) (Cached)
[wp] [Unknown] hoare_bts0513_ensures_qed_ko_ko2 (Alt-Ergo) (Cached)
[wp] [Timeout] hoare_bts0513_bis_assert_qed_ko_ko1 (Alt-Ergo) (Cached)
[wp] [Valid] hoare_bts0513_bis_assert_qed_ok_ok (Qed)
[wp] Proved goals: 1 / 4
Qed: 1
Alt-Ergo: 0 (unsuccess: 3)
......@@ -3,30 +3,30 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 24 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ASSOC_land_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L01_lnot_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L10_land_neutral_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L11_land_absorbant_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L12_land_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L13_land_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L14_land_absorbant_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L15_land_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L16_land_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L20_lor_neutral_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L21_lor_absorbant_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_L30_lxor_neutral_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_scL1_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_scN1_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_scN2_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucL1_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucL2_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucL3_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucL4_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucN1_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucN2_qed_ok : Valid
[wp] [Qed] Goal typed_cast_sgn_usgn_ensures_qed_ok_nat : Valid
[wp] [Qed] Goal typed_uchar_range_assert_qed_ok_A1 : Valid
[wp] [Qed] Goal typed_uchar_range_assert_qed_ok_A2 : Valid
[wp] [Valid] typed_lemma_ASSOC_land_qed_ok (Alt-Ergo)
[wp] [Valid] typed_lemma_L01_lnot_qed_ok (Qed)
[wp] [Valid] typed_lemma_L10_land_neutral_qed_ok (Qed)
[wp] [Valid] typed_lemma_L11_land_absorbant_qed_ok (Qed)
[wp] [Valid] typed_lemma_L12_land_qed_ok (Qed)
[wp] [Valid] typed_lemma_L13_land_qed_ok (Qed)
[wp] [Valid] typed_lemma_L14_land_absorbant_qed_ok (Qed)
[wp] [Valid] typed_lemma_L15_land_qed_ok (Qed)
[wp] [Valid] typed_lemma_L16_land_qed_ok (Qed)
[wp] [Valid] typed_lemma_L20_lor_neutral_qed_ok (Qed)
[wp] [Valid] typed_lemma_L21_lor_absorbant_qed_ok (Qed)
[wp] [Valid] typed_lemma_L30_lxor_neutral_qed_ok (Qed)
[wp] [Valid] typed_lemma_scL1_qed_ok (Qed)
[wp] [Valid] typed_lemma_scN1_qed_ok (Qed)
[wp] [Valid] typed_lemma_scN2_qed_ok (Qed)
[wp] [Valid] typed_lemma_ucL1_qed_ok (Qed)
[wp] [Valid] typed_lemma_ucL2_qed_ok (Qed)
[wp] [Valid] typed_lemma_ucL3_qed_ok (Qed)
[wp] [Valid] typed_lemma_ucL4_qed_ok (Qed)
[wp] [Valid] typed_lemma_ucN1_qed_ok (Qed)
[wp] [Valid] typed_lemma_ucN2_qed_ok (Qed)
[wp] [Valid] typed_cast_sgn_usgn_ensures_qed_ok_nat (Qed)
[wp] [Valid] typed_uchar_range_assert_qed_ok_A1 (Qed)
[wp] [Valid] typed_uchar_range_assert_qed_ok_A2 (Qed)
[wp] Proved goals: 24 / 24
Qed: 23
Alt-Ergo: 1
......@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
[wp] [Stepout] typed_cast_sgn_usgn_ensures_qed_ko_KO (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
......@@ -3,10 +3,10 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_jobA_assigns_exit : Valid
[wp] [Qed] Goal typed_jobA_assigns_normal : Valid
[wp] [Qed] Goal typed_jobG_assigns_exit : Valid
[wp] [Qed] Goal typed_jobG_assigns_normal : Valid
[wp] [Valid] typed_jobA_assigns_exit (Qed)
[wp] [Valid] typed_jobA_assigns_normal (Qed)
[wp] [Valid] typed_jobG_assigns_exit (Qed)
[wp] [Valid] typed_jobG_assigns_normal (Qed)
[wp] Proved goals: 4 / 4
Qed: 4
......@@ -3,48 +3,48 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 42 goals scheduled
[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_range_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_field_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_field_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_field_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_array_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_index_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_descr_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_comp_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_comp_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_check_FAILS : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_glob_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_check_FAILS_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_glob_check_FAILS_3 : Unsuccess
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part1 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part2 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part3 : Valid
[wp] [Valid] typed_initialize_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_initialize_loop_invariant_CHECK_established (Qed)
[wp] [Valid] typed_initialize_check_CHECK (Alt-Ergo) (Cached)
[wp] [Valid] typed_initialize_loop_assigns_part1 (Qed)
[wp] [Valid] typed_initialize_loop_assigns_part2 (Qed)
[wp] [Valid] typed_initialize_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_range_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_range_loop_assigns_part1 (Qed)
[wp] [Valid] typed_range_loop_assigns_part2 (Qed)
[wp] [Valid] typed_range_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_field_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_field_loop_assigns_part1 (Qed)
[wp] [Valid] typed_field_loop_assigns_part2 (Qed)
[wp] [Timeout] typed_array_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_array_loop_assigns_part1 (Qed)
[wp] [Valid] typed_array_loop_assigns_part2 (Qed)
[wp] [Valid] typed_array_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_index_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_index_loop_assigns_part1 (Qed)
[wp] [Valid] typed_index_loop_assigns_part2 (Qed)
[wp] [Valid] typed_index_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_descr_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_descr_loop_assigns_part1 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_descr_loop_assigns_part3 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part4 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part5 (Qed)
[wp] [Timeout] typed_comp_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_comp_loop_assigns_part1 (Qed)
[wp] [Valid] typed_comp_loop_assigns_part2 (Qed)
[wp] [Valid] typed_comp_loop_assigns_part3 (Qed)
[wp] [Unknown] typed_assigned_glob_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_loop_invariant_CHECK_established (Qed)
[wp] [Timeout] typed_assigned_glob_check_FAILS_2 (Alt-Ergo) (Cached)
[wp] [Timeout] typed_assigned_glob_check_FAILS_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_loop_assigns_part1 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_part2 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_part3 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_2_part1 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_2_part2 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_2_part3 (Qed)
[wp] Proved goals: 33 / 42
Qed: 29
Alt-Ergo: 4 (unsuccess: 9)