[wp] fixed incorrect count of proved goals

src/plugins/wp/register.ml

@@ -217,21 +217,19 @@ module GOALS = Wpo.S.Set
 
 let scheduled = ref 0
 let exercised = ref 0
-let spy = ref false
 let session = ref GOALS.empty
-let proved = ref GOALS.empty
 let provers = ref PM.empty
 
-let begin_session () = session := GOALS.empty ; spy := true
+let begin_session () = session := GOALS.empty
 let clear_session () = session := GOALS.empty
-let end_session   () = session := GOALS.empty ; spy := false
+let end_session   () = session := GOALS.empty
 let iter_session f  = GOALS.iter f !session
 
 let clear_scheduled () =
   begin
     scheduled := 0 ;
     exercised := 0 ;
-    proved := GOALS.empty ;
+    session := GOALS.empty ;
     provers := PM.empty ;
   end
 
@@ -268,7 +266,7 @@ let do_list_scheduled iter_on_goals =
     (fun goal ->
        begin
          incr scheduled ;
-         if !spy then session := GOALS.add goal !session ;
+         session := GOALS.add goal !session ;
        end) ;
   match !scheduled with
   | 0 -> Wp_parameters.warning ~current:false "No goal generated"
@@ -353,8 +351,6 @@ let do_wpo_stat goal prover res =
   | Failed | Invalid ->
       s.failed <- succ s.failed
   | Valid ->
-      if not (Wpo.is_tactic goal) then
-        proved := GOALS.add goal !proved ;
       s.proved <- succ s.proved ;
       add_step s res.prover_steps ;
       add_time s res.prover_time ;
@@ -510,12 +506,15 @@ let do_report_scheduled () =
   else
   if !scheduled > 0 then
     begin
-      let proved = GOALS.cardinal !proved in
+      let passed = GOALS.fold
+          (fun g n ->
+             if Wpo.is_passed g then succ n else n
+          ) !session 0 in
       let mode = Cache.get_mode () in
       if mode <> Cache.NoCache then do_report_cache_usage mode ;
       Wp_parameters.result "%t"
         begin fun fmt ->
-          Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
+          Format.fprintf fmt "Proved goals: %4d / %d@\n" passed !scheduled ;
           Pretty_utils.pp_items
             ~min:12 ~align:`Left
             ~title:(fun (prover,_) -> VCS.title_of_prover prover)

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle

@@ -103,7 +103,7 @@
 [wp] [Qed] Goal typed_iter_ptr_loop_assigns : Valid
 [wp] [Qed] Goal typed_iter_ptr_loop_variant_decrease : Valid
 [wp] [Alt-Ergo] Goal typed_iter_ptr_loop_variant_positive : Valid
-[wp] Proved goals:   29 / 44
+[wp] Proved goals:   44 / 44
   Qed:             0 
   Alt-Ergo:       29
 ------------------------------------------------------------

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle

@@ -39,7 +39,7 @@
 [wp] [Qed] Goal typed_exo1_assigns : Valid
 [wp] [Qed] Goal typed_exo1_loop_variant_decrease : Valid
 [wp] [Qed] Goal typed_exo1_loop_variant_positive : Valid
-[wp] Proved goals:    9 / 15
+[wp] Proved goals:   15 / 15
   Qed:             0 
   Alt-Ergo:        9
 ------------------------------------------------------------

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle

@@ -59,7 +59,7 @@
 [wp] [Qed] Goal typed_max_subarray_assigns : Valid
 [wp] [Qed] Goal typed_max_subarray_loop_variant_decrease : Valid
 [wp] [Qed] Goal typed_max_subarray_loop_variant_positive : Valid
-[wp] Proved goals:   14 / 23
+[wp] Proved goals:   23 / 23
   Qed:             0 
   Alt-Ergo:       14
 ------------------------------------------------------------

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle

@@ -106,7 +106,7 @@
 [wp] [Qed] Goal typed_ref_equal_elements_loop_variant_positive : Valid
 [wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_decrease : Valid
 [wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_positive : Valid
-[wp] Proved goals:   32 / 50
+[wp] Proved goals:   50 / 50
   Qed:            11 
   Alt-Ergo:       21
 ------------------------------------------------------------

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle

@@ -108,7 +108,7 @@
 [wp] [Qed] Goal typed_ref_equal_elements_loop_variant_positive : Valid
 [wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_decrease : Valid
 [wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_positive : Valid
-[wp] Proved goals:   34 / 51
+[wp] Proved goals:   51 / 51
   Qed:            11 
   Alt-Ergo:       23
 ------------------------------------------------------------

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle

@@ -75,7 +75,7 @@
 [wp] [Qed] Goal typed_pair_loop_variant_2_positive : Valid
 [wp] [Alt-Ergo] Goal typed_pair_has_pair_ensures : Valid
 [wp] [Alt-Ergo] Goal typed_pair_no_pair_ensures : Valid
-[wp] Proved goals:   19 / 35
+[wp] Proved goals:   35 / 35
   Qed:             4 
   Alt-Ergo:       15
 ------------------------------------------------------------

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle

@@ -270,7 +270,7 @@
 [wp] [Qed] Goal typed_size_ensures : Valid
 [wp] [Alt-Ergo] Goal typed_size_assert_rte_mem_access : Valid
 [wp] [Qed] Goal typed_size_assigns : Valid
-[wp] Proved goals:   74 / 143
+[wp] Proved goals:  143 / 143
   Qed:            16 
   Script:          1 
   Alt-Ergo:       57

src/plugins/wp/wpo.ml

@@ -805,7 +805,6 @@ let is_trivial g =
   | GoalLemma vc -> VC_Lemma.is_trivial vc
   | GoalAnnot vc -> VC_Annot.is_trivial vc
 
-
 let reduce g =
   match g.po_formula with
   | GoalLemma vc -> WpContext.on_context (get_context g) VC_Lemma.is_trivial vc
@@ -836,6 +835,12 @@ let is_unknown g = List.exists
     (fun (_,r) -> VCS.is_verdict r && not (VCS.is_valid r))
     ( get_results g )
 
+let is_passed g =
+  if is_smoke_test g then
+    not (is_proved g)
+  else
+    is_proved g
+
 let get_result =
   Dynamic.register ~plugin:"Wp" "Wpo.get_result" ~journalize:false
     (Datatype.func2 WpoType.ty ProverType.ty ResultType.ty)

src/plugins/wp/wpo.mli

@@ -159,7 +159,8 @@ val get_proof : t -> [`Passed|`Failed|`Unknown] * Property.t
 val get_target : t -> Property.t
 val is_trivial : t -> bool (** do not tries simplification, do not check prover results *)
 val is_proved : t -> bool (** do not tries simplification, check prover results *)
-val is_unknown : t -> bool
+val is_unknown : t -> bool (** at least one prover returns « Unknown » *)
+val is_passed : t -> bool (** proved, or unknown for smoke tests *)
 val warnings : t -> Warning.t list
 
 (** [true] if the result is valid. Dynamically exported.