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

[wp] updated oracles

parent c3ee29ac
......@@ -152,13 +152,13 @@ let results ~smoke prs =
else
let cached = List.fold_left
(fun c (_,r) -> if r.VCS.cached then succ c else c)
0 doomed in
0 passed in
let stucked = List.map
(fun (p,r) -> p, ptime r.prover_time true)
doomed in
passed in
let solver = List.fold_left
(fun t (_,r) -> t +. r.solver_time)
0.0 doomed in
0.0 passed in
let provers = pmerge [Qed,ptime solver false] stucked in
let verdict =
if missing <> [] then NoResult else
......@@ -166,7 +166,7 @@ let results ~smoke prs =
| [] -> NoResult
| u::w -> (snd @@ List.fold_left choose_worst u w).verdict in
let proved = List.length passed in
let failed = List.length missing + List.length doomed in
let failed = List.length missing in
{ empty with verdict ; provers ; cached ; proved ; failed }
let add a b =
......
......@@ -330,14 +330,14 @@ let do_wpo_success ~shell ~updating goal success =
else
let smoke = Wpo.is_smoke_test goal in
let stats = ProofEngine.consolidated goal in
let proof, target = Wpo.get_proof goal in
begin
if shell || stats.verdict <> Valid then
if shell || proof <> `Passed then
do_report_stats ~shell ~updating goal ~smoke stats ;
if smoke && stats.verdict <> Valid then
if smoke && proof <> `Passed then
begin
let target = Wpo.get_target goal in
let source = fst (Property.location target) in
Wp_parameters.warning ~source "Failed smoke-test"
Wp_parameters.warning ~once:true ~source "Failed smoke-test"
end ;
end
......
......@@ -6,17 +6,17 @@
[wp] [Valid] typed_globals_check_qed_ok (Qed)
[wp] [Valid] typed_globals_check_qed_ok_2 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_3 (Qed)
[wp] [Unknown] typed_globals_check_qed_ko (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_4 (Qed)
[wp] [Unknown] typed_globals_check_qed_ko_2 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_5 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_6 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_7 (Qed)
[wp] [Valid] typed_globals_check_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_2 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_not_provable (Alt-Ergo)
[wp] [Unknown] typed_globals_check_not_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_3 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_qed_ko_3 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_8 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_9 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_10 (Qed)
......@@ -27,13 +27,13 @@
[wp] [Valid] typed_globals_check_provable_5 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_6 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_7 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_qed_ko_4 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko_5 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko_6 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko_7 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_not_provable_2 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_not_provable_3 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_not_provable_4 (Alt-Ergo)
[wp] [Unknown] typed_globals_check_qed_ko_4 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_qed_ko_5 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_qed_ko_6 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_qed_ko_7 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_not_provable_2 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_not_provable_3 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_globals_check_not_provable_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_locals_check_qed_ok (Qed)
[wp] [Valid] typed_locals_check_qed_ok_2 (Qed)
[wp] [Valid] typed_locals_check_qed_ok_3 (Qed)
......@@ -75,7 +75,7 @@
[wp] [Valid] typed_complex_struct_check_qed_ok_16 (Qed)
[wp] [Valid] typed_complex_struct_check_qed_ok_17 (Qed)
[wp] [Valid] typed_complex_struct_check_qed_ok_18 (Qed)
[wp] [Valid] typed_complex_struct_check_provable (Script)
[wp] [Valid] typed_complex_struct_check_provable (Script) (Qed 2/2)
[wp] Proved goals: 62 / 73
Qed: 52
Script: 1
......
......@@ -19,7 +19,7 @@
[wp] [Valid] typed_BinaryMultiplication_loop_assigns (Qed)
[wp] [Valid] typed_BinaryMultiplication_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] [Valid] typed_BinaryMultiplication_loop_variant_positive (Qed)
[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Script)
[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Script 4) (Qed 1/10) (Alt-Ergo 9/10) (Cached)
[wp] Proved goals: 17 / 17
Qed: 4
Script: 1
......
......@@ -3,13 +3,13 @@
[wp] Running WP plugin...
[rte:annot] annotating function binary_search
[wp] 28 goals scheduled
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_loop_s3 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s17 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s18 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_loop_s3 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s17 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_binary_search_ensures_Result (Alt-Ergo) (Cached)
[wp] [Valid] typed_binary_search_ensures_Found (Qed)
[wp] [Valid] typed_binary_search_ensures_NotFound (Alt-Ergo) (Cached)
......
......@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[rte:annot] annotating function euclid_gcd
[wp] 16 goals scheduled
[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_ensures (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_established (Qed)
......
......@@ -2,8 +2,8 @@
[kernel] Parsing bitmask0x8000.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Valid] typed_lemma_res_n (Script)
[wp] [Valid] typed_lemma_res_y (Script)
[wp] [Valid] typed_lemma_res_n (Script) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
[wp] [Valid] typed_lemma_res_y (Script) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
......
......@@ -3,13 +3,13 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
[wp] [Failed (Doomed)] typed_foo_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_foo_wp_smoke_A_requires (Qed)
[wp] [Passed (Timeout)] typed_foo_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_A_requires (Qed)
[wp] doomed.i:27: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_foo_wp_smoke_B_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_bar_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_foo_wp_smoke_B_requires (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_bar_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Valid] typed_bar_ensures (Qed)
[wp] [Passed (Invalid)] typed_buzz_wp_smoke_default_requires (Qed)
[wp] [Failed (Doomed)] typed_buzz_wp_smoke_default_requires (Qed)
[wp] doomed.i:41: Warning: Failed smoke-test
[wp] [Valid] typed_buzz_ensures (Qed)
[wp] Proved goals: 5 / 7
......
......@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:29: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:30: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:32: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
......
......@@ -3,43 +3,42 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_ensures (Qed)
[wp] [Valid] typed_f1_ok_exits (Qed)
[wp] [Failed (Doomed)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_ensures (Qed)
[wp] [Valid] typed_f2_ok_exits (Qed)
[wp] [Passed (Invalid)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] [Failed (Doomed)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] doomed_call.i:68: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] [Failed (Doomed)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Valid] typed_f3_ko_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_ensures (Qed)
[wp] [Passed (Invalid)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Valid] typed_f4_ko_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Passed (Unknown)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 28 / 33
Qed: 10 (failed: 5)
......
......@@ -3,46 +3,45 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_ensures_part1 (Qed)
[wp] [Valid] typed_f1_ok_ensures_part2 (Qed)
[wp] [Valid] typed_f1_ok_exits (Qed)
[wp] [Failed (Doomed)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_ensures_part1 (Qed)
[wp] [Valid] typed_f2_ok_ensures_part2 (Qed)
[wp] [Valid] typed_f2_ok_exits_part1 (Qed)
[wp] [Valid] typed_f2_ok_exits_part2 (Qed)
[wp] [Passed (Invalid)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] [Failed (Doomed)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] doomed_call.i:68: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] [Failed (Doomed)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Valid] typed_f3_ko_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_ensures (Qed)
[wp] [Passed (Invalid)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Valid] typed_f4_ko_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_ensures (Qed)
[wp] [Failed (Doomed)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Passed (Unknown)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 31 / 36
Qed: 13 (failed: 5)
......
......@@ -3,50 +3,50 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 46 goals scheduled
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part2 (Qed)
[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_assigns_exit (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part2 (Qed)
[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] doomed_dead.i:44: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ko_assigns_exit (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part2 (Qed)
[wp] [Failed (Doomed)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_assigns_exit (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part2 (Qed)
[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_assert (Qed)
[wp] [Valid] typed_f4_ok_assigns_exit (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part3 (Qed)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part3 (Qed)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] doomed_dead.i:90: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ko_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
......
......@@ -3,52 +3,52 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 48 goals scheduled
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part3 (Qed)
[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_assigns_exit (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part3 (Qed)
[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] doomed_dead.i:44: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ko_assigns_exit (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part2 (Qed)
[wp] [Failed (Doomed)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_assigns_exit (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part2 (Qed)
[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_assert (Qed)
[wp] [Valid] typed_f4_ok_assigns_exit (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part3 (Qed)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part3 (Qed)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] doomed_dead.i:90: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ko_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
......
......@@ -3,8 +3,8 @@
[wp] Running WP plugin...
[rte:annot] annotating function access
[wp] 4 goals scheduled
[wp] [Failed (Doomed)] typed_access_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_access_wp_smoke_dead_code_s5 (Qed)
[wp] [Passed (Unknown)] typed_access_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_access_wp_smoke_dead_code_s5 (Qed)
[wp] doomed_localinit.i:11: Warning: Failed smoke-test
[wp] [Timeout] typed_access_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Timeout] typed_access_assert_rte_mem_access_2 (Alt-Ergo) (Cached)
......
......@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Qed)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Qed)
[wp] doomed_loop.i:22: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Qed)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Qed)
[wp] doomed_loop.i:23: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Qed)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Qed)
[wp] doomed_loop.i:25: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Qed)
[wp] [Unknown] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
......
......@@ -3,27 +3,26 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
[wp] [Passed (Invalid)] typed_requires_wp_smoke_default_requires (Qed)
[wp] [Failed (Doomed)] typed_requires_wp_smoke_default_requires (Qed)
[wp] doomed_pre.i:10: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_reqs_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_reqs_assumes_wp_smoke_B_assumes (Qed)
[wp] [Passed (Timeout)] typed_reqs_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_reqs_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:16: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_reqs_2_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_reqs_2_2_assumes_wp_smoke_B_assumes (Qed)
[wp] [Passed (Timeout)] typed_reqs_2_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_reqs_2_2_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:23: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_reqs_1_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_reqs_1_2_assumes_wp_smoke_B_assumes (Qed)
[wp] [Passed (Timeout)] typed_reqs_1_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_reqs_1_2_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:30: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_reqs_combined_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_reqs_combined_assumes_wp_smoke_B_assumes (Qed)
[wp] [Passed (Unknown)] typed_reqs_combined_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_reqs_combined_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:37: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_bhv_requires_assumes_wp_smoke_B_requires (Qed)
[wp] [Failed (Doomed)] typed_bhv_requires_assumes_wp_smoke_B_requires (Qed)
[wp] doomed_pre.i:48: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed (Invalid)] typed_reqs_massumes_wp_smoke_B1_assumes (Qed)
[wp] doomed_pre.i:56: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
[wp] [Passed (Timeout)] typed_reqs_massumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_B1_assumes (Qed)
[wp] doomed_pre.i:56: Warning: Failed smoke-test
[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
[wp] Proved goals: 5 / 13
Qed: 0 (failed: 8)
Alt-Ergo: 5
......
......@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:30: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
......
......@@ -3,9 +3,9 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[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)
......
......@@ -6,9 +6,9 @@
[wp] doomed_unreach.i:22: Warning: Failed smoke-test
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s5 (Alt-Ergo) (Cached)
[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
[wp] [Passed (Unknown)] typed_job_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)