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

[wp] fix console for valid results

parent 0e692305
No related branches found
No related tags found
No related merge requests found
...@@ -334,17 +334,19 @@ let do_wpo_success ~shell ~cache goal success = ...@@ -334,17 +334,19 @@ let do_wpo_success ~shell ~cache goal success =
let smoke = Wpo.is_smoke_test goal in let smoke = Wpo.is_smoke_test goal in
let gstats = Stats.results ~smoke @@ Wpo.get_results goal in let gstats = Stats.results ~smoke @@ Wpo.get_results goal in
let cstats = ProofEngine.consolidated goal in let cstats = ProofEngine.consolidated goal in
let proof, target = Wpo.get_proof goal in let success = Wpo.is_passed goal in
begin begin
global_stats := Stats.add !global_stats gstats ; global_stats := Stats.add !global_stats gstats ;
if cstats.tactics > 0 then if cstats.tactics > 0 then
script_stats := Stats.add !script_stats cstats ; script_stats := Stats.add !script_stats cstats ;
if shell || proof <> `Passed then if shell || not success then
do_report_stats ~shell ~cache goal ~smoke cstats ; do_report_stats ~shell ~cache goal ~smoke cstats ;
if smoke && proof <> `Passed then if smoke then
begin begin
let source = fst (Property.location target) in let proof, target = Wpo.get_proof goal in
Wp_parameters.warning ~once:true ~source "Failed smoke-test" if proof <> `Passed then
let source = fst (Property.location target) in
Wp_parameters.warning ~once:true ~source "Failed smoke-test"
end ; end ;
end end
......
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