[wp] consolidated JSON report, script stats details

f21d56de · Loïc Correnson · Allan Blanchard · 80f68164 · f21d56de · f21d56de
Commit f21d56de authored Jul 12, 2022 by Loïc Correnson Committed by Allan Blanchard Jul 28, 2022
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -232,9 +232,9 @@ let pp_stats ~shell ~updating fmt s =
  let vp = s.proved in
  let np = proofs s in
  if s.tactics > 1 then
-    Format.fprintf fmt " (Script %d)" s.tactics
+    Format.fprintf fmt " (Tactics %d)" s.tactics
  else if s.tactics = 1 then
-    Format.fprintf fmt " (Script)" ;
+    Format.fprintf fmt " (Tactic)" ;
  let perfo = not shell || (not updating && s.cached < vp) in
  let qed_only =
    match s.provers with [Qed,_] -> vp = np | _ -> false in
@@ -268,26 +268,3 @@ let pp_stats ~shell ~updating fmt s =
 let pretty = pp_stats ~shell:false ~updating:false

 (* -------------------------------------------------------------------------- *)
-(* --- Yojson                                                             --- *)
-(* -------------------------------------------------------------------------- *)
-
-let pstats_to_json (p,r) : Json.t = `Assoc [
-    "prover", `String (VCS.name_of_prover p) ;
-    "hprover", `String (VCS.title_of_prover p) ;
-    "time", `Float r.time ;
-    "htime", `String (Pretty_utils.to_string Rformat.pp_time r.time) ;
-    "success", `Int (truncate r.success) ;
-  ]
-
-let stats_to_json s : Json.t = `Assoc [
-    "provers", `List (List.map pstats_to_json s.provers);
-    "tactics", `Int s.tactics;
-    "proved", `Int s.proved;
-    "timeout", `Int s.timeout;
-    "unknown", `Int s.unknown ;
-    "noresult", `Int s.noresult ;
-    "failed", `Int s.failed ;
-    "cached", `Int s.cached ;
-  ]
-
-(* -------------------------------------------------------------------------- *)
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -61,6 +61,4 @@ val script : stats -> VCS.result
 val proofs : stats -> int
 val complete : stats -> bool

-val stats_to_json : stats -> Json.t
-
 (* -------------------------------------------------------------------------- *)
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -310,6 +310,15 @@ let pp_perf_shell fmt r =
  if not (Wp_parameters.has_dkey dkey_shell) then
    pp_perf_forced fmt r

+let name_of_verdict = function
+  | NoResult | Computing _ -> "none"
+  | Invalid -> "invalid"
+  | Valid -> "valid"
+  | Failed -> "failed"
+  | Unknown -> "unknown"
+  | Stepout -> "stepout"
+  | Timeout -> "timeout"
+
 let pp_result fmt r =
  match r.verdict with
  | NoResult -> Format.pp_print_string fmt "No Result"

--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -124,6 +124,8 @@ val verdict: smoke:bool -> result -> verdict
 val configure : result -> config
 val autofit : result -> bool (** Result that fits the default configuration *)

+val name_of_verdict : verdict -> string
+
 val pp_result : Format.formatter -> result -> unit
 val pp_result_qualif : ?updating:bool -> prover -> result ->
  Format.formatter -> unit

--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -86,7 +86,7 @@ let do_wp_print_for goals =
 let do_wp_report model =
  begin
    let reports = Wp_parameters.Report.get () in
-    let jreport = Wp_parameters.ReportJson.get () in
+    let jreport = Wp_parameters.OldReportJson.get () in
    if reports <> [] || jreport <> "" then
      begin
        let stats = WpReport.fcstat () in
@@ -98,7 +98,8 @@ let do_wp_report model =
          | [jinput;joutput] ->
            WpReport.export_json stats ~jinput ~joutput () ;
          | _ ->
-            Wp_parameters.error "Invalid format for option -wp-report-json"
+            Wp_parameters.error
+              "Invalid format for option -wp-deprecated-report-json"
        end ;
        List.iter (WpReport.export stats) reports ;
      end ;
@@ -132,14 +133,16 @@ module GOALS = Wpo.S.Set
 let scheduled = ref 0
 let exercised = ref 0
 let session = ref GOALS.empty
-let global = ref Stats.empty
+let global_stats = ref Stats.empty
+let script_stats = ref Stats.empty

 let clear_scheduled () =
  begin
    scheduled := 0 ;
    exercised := 0 ;
    session := GOALS.empty ;
-    global := Stats.empty ;
+    global_stats := Stats.empty ;
+    script_stats := Stats.empty ;
    CfgInfos.trivial_terminates := 0 ;
    WpReached.unreachable_proved := 0 ;
    WpReached.unreachable_failed := 0 ;
@@ -218,6 +221,72 @@ let do_report_cache_usage mode =
            Format.pp_print_newline fmt () ;
        end

+(* -------------------------------------------------------------------------- *)
+(* --- Prover JSON Results                                                --- *)
+(* -------------------------------------------------------------------------- *)
+
+let pstats_to_json (p,r) : Json.t = `Assoc [
+    "prover", `String (VCS.name_of_prover p) ;
+    "time", `Float r.Stats.time ;
+    "success", `Int (truncate r.Stats.success) ;
+  ]
+
+let stats_to_json g (s : Stats.stats) : Json.t =
+  let smoke = Wpo.is_smoke_test g in
+  let target = Wpo.get_target g in
+  let source = fst (Property.location target) in
+  let script = match ProofSession.get g with
+    | NoScript -> []
+    | Script file | Deprecated file -> [ "script", `String file ]
+  in
+  let index =
+    match g.po_idx with
+    | Axiomatic None -> []
+    | Axiomatic (Some ax) ->
+      [ "axiomatic", `String ax ]
+    | Function(kf,None) ->
+      [ "function", `String (Kernel_function.get_name kf) ]
+    | Function(kf,Some bhv) -> [
+        "function", `String (Kernel_function.get_name kf);
+        "behavior", `String bhv ;
+      ] in
+  `Assoc
+    ([
+      "goal", `String g.po_gid ;
+      "property", `String (Property.Names.get_prop_name_id target) ;
+      "file", `String (source.pos_path :> string) ;
+      "line", `Int source.pos_lnum ;
+    ] @ index @ [
+        "smoke", `Bool smoke ;
+        "passed", `Bool (Wpo.is_passed g) ;
+        "verdict", `String (VCS.name_of_verdict s.verdict) ;
+      ] @ script @ [
+        "provers", `List (List.map pstats_to_json s.provers) ;
+      ] @
+      List.filter (function (_,`Int n) -> n > 0 | _ -> true) [
+        "tactics", `Int s.tactics;
+        "proved", `Int s.proved;
+        "timeout", `Int s.timeout;
+        "unknown", `Int s.unknown ;
+        "noresult", `Int s.noresult ;
+        "failed", `Int s.failed ;
+        "cached", `Int s.cached ;
+      ])
+
+let do_report_json () =
+  let file = Wp_parameters.ReportJson.get () in
+  if file <> "" then
+    let json = List.rev @@
+      GOALS.fold
+        (fun g json ->
+           let s = ProofEngine.consolidated g in
+           let js = stats_to_json g s in
+           js :: json
+        ) !session [] in
+    let pretty =
+      Wp_parameters.verbose_atleast 2 || Wp_parameters.debug_atleast 1 in
+    Json.save_file ~pretty file (`List json)
+
 (* -------------------------------------------------------------------------- *)
 (* --- Prover Results                                                     --- *)
 (* -------------------------------------------------------------------------- *)
@@ -263,12 +332,14 @@ let do_wpo_success ~shell ~updating goal success =
  else
    let smoke = Wpo.is_smoke_test goal in
    let gstats = Stats.results ~smoke @@ Wpo.get_results goal in
-    let stats = ProofEngine.consolidated goal in
+    let cstats = ProofEngine.consolidated goal in
    let proof, target = Wpo.get_proof goal in
    begin
-      global := Stats.add !global gstats ;
+      global_stats := Stats.add !global_stats gstats ;
+      if cstats.tactics > 0 then
+        script_stats := Stats.add !script_stats cstats ;
      if shell || proof <> `Passed then
-        do_report_stats ~shell ~updating goal ~smoke stats ;
+        do_report_stats ~shell ~updating goal ~smoke cstats ;
      if smoke && proof <> `Passed then
        begin
          let source = fst (Property.location target) in
@@ -288,7 +359,7 @@ let do_report_scheduled () =
      !CfgInfos.trivial_terminates in
    if total > 0 then
      begin
-        let gstats = !global in
+        let gstats = !global_stats in
        let unreachable = !WpReached.unreachable_proved in
        let terminating = !CfgInfos.trivial_terminates in
        let passed = GOALS.fold
@@ -296,6 +367,7 @@ let do_report_scheduled () =
               if Wpo.is_passed g then succ n else n
            ) !session (unreachable + terminating) in
        let mode = Cache.get_mode () in
+        let updating = Cache.is_updating () in
        if mode <> Cache.NoCache then do_report_cache_usage mode ;
        let shell = Wp_parameters.has_dkey VCS.dkey_shell in
        let lines = ref [] in
@@ -309,9 +381,12 @@ let do_report_scheduled () =
             let name = VCS.title_of_prover p in
             let success = truncate s.Stats.success in
             if success > 0 || (not shell && p = Qed) then
-             add_line name success (fun fmt ->
-                 if shell then Stats.pp_pstats fmt s
-               )
+               add_line name success (fun fmt ->
+                   if p = Tactical then
+                     Stats.pp_stats ~shell ~updating fmt !script_stats
+                   else
+                   if not shell then Stats.pp_pstats fmt s
+                 )
          ) gstats.provers ;
        if gstats.failed > 0 then add_line "Failed" gstats.failed none ;
        if not shell then
@@ -335,6 +410,7 @@ let do_report_scheduled () =
 let do_list_scheduled_result () =
  begin
    do_report_scheduled () ;
+    do_report_json () ;
    clear_scheduled () ;
  end


--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -75,10 +75,10 @@
 [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) (Qed 2/2)
+[wp] [Valid] typed_complex_struct_check_provable (Tactic) (Qed 2/2)
 [wp] Proved goals:   62 / 73
  Qed:            52
-  Script:          1
+  Script:          1 (Tactic) (Qed 2/2)
  Alt-Ergo:        9
 ------------------------------------------------------------
 Functions                 WP     Alt-Ergo  Total   Success

--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -19,10 +19,10 @@
 [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 4) (Qed 1/10) (Alt-Ergo 9/10) (Cached)
+[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Tactics 4) (Qed 1/10) (Alt-Ergo 9/10) (Cached)
 [wp] Proved goals:   17 / 17
  Qed:             4
-  Script:          1
+  Script:          1 (Tactics 4) (Qed 1/10) (Alt-Ergo 9/10) (Cached)
  Alt-Ergo:       12
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success

--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
@@ -2,10 +2,10 @@
 [kernel] Parsing bitmask0x8000.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] 2 goals scheduled
-[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] [Valid] typed_lemma_res_n (Tactic) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
+[wp] [Valid] typed_lemma_res_y (Tactic) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
 [wp] Proved goals:    2 / 2
-  Script:          2
+  Script:          2 (Tactics 2) (Qed 2/4) (Alt-Ergo 2/4) (Cached)
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success
  Lemma                     -        -        2       100%

--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
@@ -4,9 +4,9 @@
 [wp] Warning: Missing RTE guards
 [wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
 [wp] 1 goal scheduled
-[wp] [Valid] typed_unrolled_loop_ensures_zero (Script 2) (Qed 18/18)
+[wp] [Valid] typed_unrolled_loop_ensures_zero (Tactics 2) (Qed 18/18)
 [wp] Proved goals:    1 / 1
-  Script:          1
+  Script:          1 (Tactics 2) (Qed 18/18)
 ------------------------------------------------------------
 Functions                 WP     Alt-Ergo  Total   Success
  unrolled_loop             -        -        1       100%

--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing unsigned.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_U32 (Script)
+[wp] [Unsuccess] typed_lemma_U32 (Tactic)
 [wp] Proved goals:    0 / 1
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success

--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -105,7 +105,7 @@
  Prove: P_S(42).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_clear_in_step_check (Script 3)
+[wp] [Unsuccess] typed_clear_in_step_check (Tactics 3)
 [wp:script:allgoals] 
  typed_clear_ensures subgoal:
  
@@ -143,5 +143,5 @@
  Prove: P_S(a + b).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_clear_ensures (Script 7)
+[wp] [Unsuccess] typed_clear_ensures (Tactics 7)
 [wp] Proved goals:    0 / 2
--- a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
@@ -54,7 +54,7 @@
  Prove: false.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_function_loop_invariant_X_preserved (Script)
+[wp] [Unsuccess] typed_function_loop_invariant_X_preserved (Tactic)
 [wp:script:allgoals] 
  typed_function_loop_invariant_X_preserved subgoal:
  

--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -14,7 +14,7 @@
  Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
  
  ------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Script) (Qed 2/2)
+[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Tactic) (Qed 2/2)
 [wp:script:allgoals] 
  typed_check_lemma_and_modulo_u subgoal:
  
@@ -56,6 +56,6 @@
  Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
  
  ------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_u (Script 4) (Qed 37/37)
+[wp] [Valid] typed_check_lemma_and_modulo_u (Tactics 4) (Qed 37/37)
 [wp] Proved goals:    2 / 2
-  Script:          2
+  Script:          2 (Tactics 5) (Qed 39/39)
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -14,7 +14,7 @@
  Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
  
  ------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Script) (Qed 2/2)
+[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Tactic) (Qed 2/2)
 [wp:script:allgoals] 
  typed_check_lemma_and_modulo_u subgoal:
  
@@ -56,6 +56,6 @@
  Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
  
  ------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_u (Script 4) (Qed 37/37)
+[wp] [Valid] typed_check_lemma_and_modulo_u (Tactics 4) (Qed 37/37)
 [wp] Proved goals:    2 / 2
-  Script:          2
+  Script:          2 (Tactics 5) (Qed 39/39)
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -201,7 +201,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_branch_ensures (Script)
+[wp] [Unsuccess] typed_test_step_branch_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_branch_ensures subgoal:
  
@@ -224,7 +224,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_or_ensures (Script)
+[wp] [Unsuccess] typed_test_step_or_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_or_ensures subgoal:
  
@@ -256,7 +256,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_and_ensures (Script)
+[wp] [Unsuccess] typed_test_step_and_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_peq_ensures subgoal:
  
@@ -265,7 +265,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_peq_ensures (Script)
+[wp] [Unsuccess] typed_test_step_peq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_peq_ensures subgoal:
  
@@ -282,7 +282,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_pneq_ensures (Script)
+[wp] [Unsuccess] typed_test_step_pneq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_pneq_ensures subgoal:
  
@@ -299,7 +299,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_neq_ensures (Script)
+[wp] [Unsuccess] typed_test_step_neq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_neq_ensures subgoal:
  
@@ -324,7 +324,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_leq_ensures (Script)
+[wp] [Unsuccess] typed_test_step_leq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_leq_ensures subgoal:
  
@@ -354,7 +354,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_lt_ensures (Script)
+[wp] [Unsuccess] typed_test_step_lt_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_lt_ensures subgoal:
  
@@ -379,7 +379,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_if_ensures (Script)
+[wp] [Unsuccess] typed_test_step_if_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_if_ensures subgoal:
  
@@ -405,7 +405,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_if_ensures (Script)
+[wp] [Unsuccess] typed_test_step_fa_if_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_fa_if_ensures subgoal:
  
@@ -427,7 +427,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_or_ensures (Script)
+[wp] [Unsuccess] typed_test_step_fa_or_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_step_fa_or_ensures subgoal:
  
@@ -448,7 +448,7 @@
  Prove: P_S.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_and_ensures (Script)
+[wp] [Unsuccess] typed_test_step_fa_and_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_inside_leq_ensures subgoal:
  
@@ -463,7 +463,7 @@
  Prove: P_Q.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_leq_ensures (Script)
+[wp] [Unsuccess] typed_test_inside_leq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_inside_leq_ensures subgoal:
  
@@ -494,7 +494,7 @@
  Prove: P_Q.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_lt_ensures (Script)
+[wp] [Unsuccess] typed_test_inside_lt_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_inside_lt_ensures subgoal:
  
@@ -525,7 +525,7 @@
  Prove: P_Q.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_neq_ensures (Script)
+[wp] [Unsuccess] typed_test_inside_neq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_inside_neq_ensures subgoal:
  
@@ -556,7 +556,7 @@
  Prove: P_P.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_and_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_and_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_and_ensures subgoal:
  
@@ -581,7 +581,7 @@
  Prove: (L_LP=true).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_eq_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_eq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_eq_ensures subgoal:
  
@@ -598,7 +598,7 @@
  Prove: (L_LP=false).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_neq_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_neq_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_neq_ensures subgoal:
  
@@ -620,7 +620,7 @@
  Prove: P_P.
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_if_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_if_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_if_ensures subgoal:
  
@@ -642,7 +642,7 @@
  Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_ex_and_ensures subgoal:
  
@@ -659,7 +659,7 @@
  Prove: P_P \/ P_Q \/ (exists i : Z. P_Pi(i)) \/ (exists i : Z. P_Qi(i)).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_or_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_ex_or_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_ex_if_ensures subgoal:
  
@@ -674,7 +674,7 @@
  Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_if_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_ex_if_ensures (Tactic)
 [wp:script:allgoals] 
  typed_test_goal_ex_if_ensures subgoal:
  
@@ -702,5 +702,5 @@
  Prove: exists i : Z. P_Qi(i).
  
  ------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_imply_ensures (Script)
+[wp] [Unsuccess] typed_test_goal_ex_imply_ensures (Tactic)
 [wp] Proved goals:    0 / 23
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
@@ -2,9 +2,9 @@
 [kernel] Parsing induction.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] 1 goal scheduled
-[wp] [Valid] typed_lemma_ByInd (Script) (Alt-Ergo 3/3) (Cached)
+[wp] [Valid] typed_lemma_ByInd (Tactic) (Alt-Ergo 3/3) (Cached)
 [wp] Proved goals:    1 / 1
-  Script:          1
+  Script:          1 (Tactic) (Alt-Ergo 3/3) (Cached)
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success
  Axiomatic Inductive       -        -        1       100%

--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing induction.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_ByInd (Script)
+[wp] [Unsuccess] typed_lemma_ByInd (Tactic)
 [wp] Proved goals:    0 / 1
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success

--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing induction.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_ByInd (Script)
+[wp] [Unsuccess] typed_lemma_ByInd (Tactic)
 [wp] Proved goals:    0 / 1
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success

--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
@@ -2,10 +2,10 @@
 [kernel] Parsing overflow.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] 2 goals scheduled
-[wp] [Valid] typed_lemma_j_incr_char (Script) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
-[wp] [Valid] typed_lemma_j_incr_short (Script) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
+[wp] [Valid] typed_lemma_j_incr_char (Tactic) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
+[wp] [Valid] typed_lemma_j_incr_short (Tactic) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
 [wp] Proved goals:    2 / 2
-  Script:          2
+  Script:          2 (Tactics 2) (Qed 2/6) (Alt-Ergo 4/6) (Cached)
 ------------------------------------------------------------
 Axiomatics                WP     Alt-Ergo  Total   Success
  Lemma                     -        -        2       100%

--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
@@ -3,11 +3,11 @@
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_Or (Script)
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And (Script)
-[wp] [Unsuccess] ty