Merge branch 'fix/wp/terminates-result-display' into 'master'

Fix trivial terminates proof display + count

See merge request frama-c/frama-c!3260

src/plugins/wp/register.ml

@@ -182,6 +182,7 @@ let clear_scheduled () =
     exercised := 0 ;
     session := GOALS.empty ;
     provers := PM.empty ;
+    WpAnnot.trivial_terminates := 0 ;
     WpAnnot.unreachable_proved := 0 ;
     WpAnnot.unreachable_failed := 0 ;
   end
@@ -462,13 +463,19 @@ let do_report_scheduled () =
     Wp_parameters.result "%d goal%s generated" !exercised plural
   else
     let total =
-      !scheduled + !WpAnnot.unreachable_failed + !WpAnnot.unreachable_proved in
+      !scheduled +
+      !WpAnnot.unreachable_failed +
+      !WpAnnot.unreachable_proved +
+      !WpAnnot.trivial_terminates in
     if total > 0 then
       begin
+        let passed =
+          !WpAnnot.unreachable_proved + !WpAnnot.trivial_terminates
+        in
         let passed = GOALS.fold
             (fun g n ->
                if Wpo.is_passed g then succ n else n
-            ) !session !WpAnnot.unreachable_proved in
+            ) !session passed in
         let mode = Cache.get_mode () in
         if mode <> Cache.NoCache then do_report_cache_usage mode ;
         Wp_parameters.result "%t"

src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle

@@ -4,6 +4,7 @@
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/terminates_call_options.c:20: Warning: 
   Missing terminates clause for definition, populates 'terminates \true'
+[wp] [CFG] Goal definition_terminates : Valid (Trivial)
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:17: Warning: 

src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle

@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_acsl/terminates_formulae.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal variant_terminates : Valid (Trivial)
 ------------------------------------------------------------
   Function base_call
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
 ------------------------------------------------------------
   Function f1
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
 [wp] tests/wp_acsl/terminates_variant_option.i:52: Warning: 
   Loop variant is always trivially verified (terminates \false)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
 [wp] tests/wp_acsl/terminates_variant_option.i:59: Warning: 
   Loop variant is always trivially verified (terminates \false)
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle

@@ -4,6 +4,7 @@
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/terminates_call_options.c:20: Warning: 
   Missing terminates clause for definition, populates 'terminates \true'
+[wp] [CFG] Goal definition_terminates : Valid (Trivial)
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:17: Warning: 
@@ -20,7 +21,7 @@
 [wp] [Qed] Goal typed_call_definition_terminates : Valid
 [wp] [Alt-Ergo] Goal typed_no_spec_generates_goal_terminates : Unsuccess
 [wp] [Qed] Goal typed_libc_call_terminates : Valid
-[wp] Proved goals:    4 / 5
+[wp] Proved goals:    5 / 6
   Qed:             4 
   Alt-Ergo:        0  (unsuccess: 1)
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle

@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_acsl/terminates_formulae.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal variant_terminates : Valid (Trivial)
 [wp] 10 goals scheduled
 [wp] [Alt-Ergo] Goal typed_base_call_terminates : Unsuccess
 [wp] [Qed] Goal typed_call_same_terminates : Valid
@@ -13,7 +14,7 @@
 [wp] [Qed] Goal typed_variant_loop_variant_positive : Valid
 [wp] [Alt-Ergo] Goal typed_no_variant_terminates : Unsuccess
 [wp] [Qed] Goal typed_no_variant_loop_assigns : Valid
-[wp] Proved goals:    6 / 10
+[wp] Proved goals:    7 / 11
   Qed:             5 
   Alt-Ergo:        1  (unsuccess: 4)
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
 [wp] 20 goals scheduled
 [wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
 [wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
@@ -23,7 +27,7 @@
 [wp] [Qed] Goal typed_trivial_variant_default_loop_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_trivial_variant_default_loop_variant_decrease : Unsuccess
 [wp] [Alt-Ergo] Goal typed_trivial_variant_default_loop_variant_positive : Unsuccess
-[wp] Proved goals:   13 / 20
+[wp] Proved goals:   17 / 24
   Qed:            10 
   Alt-Ergo:        3  (unsuccess: 7)
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
 [wp] tests/wp_acsl/terminates_variant_option.i:52: Warning: 
   Loop variant is always trivially verified (terminates \false)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
 [wp] tests/wp_acsl/terminates_variant_option.i:59: Warning: 
   Loop variant is always trivially verified (terminates \false)
 [wp] 20 goals scheduled
@@ -27,7 +31,7 @@
 [wp] [Qed] Goal typed_trivial_variant_default_loop_assigns : Valid
 [wp] [Qed] Goal typed_trivial_variant_default_loop_variant_decrease : Valid
 [wp] [Qed] Goal typed_trivial_variant_default_loop_variant_positive : Valid
-[wp] Proved goals:   20 / 20
+[wp] Proved goals:   24 / 24
   Qed:            16 
   Alt-Ergo:        4
 ------------------------------------------------------------

src/plugins/wp/wpAnnot.ml

@@ -79,6 +79,9 @@ let set_unreachable pid =
 (* -------------------------------------------------------------------------- *)
 (* --- Status of Terminates Annotations                                   --- *)
 (* -------------------------------------------------------------------------- *)
+
+let trivial_terminates = ref 0
+
 let wp_trivially_terminates =
   Emitter.create
     "Trivial Termination"
@@ -87,6 +90,8 @@ let wp_trivially_terminates =
     ~tuning:[] (* TBC *)
 
 let set_trivially_terminates p =
+  incr trivial_terminates ;
+  Wp_parameters.result "[CFG] Goal %a : Valid (Trivial)" WpPropId.pp_propid p ;
   let pid = WpPropId.property_of_id p in
   Property_status.emit wp_trivially_terminates ~hyps:[] pid Property_status.True
 

src/plugins/wp/wpAnnot.mli

@@ -34,6 +34,7 @@ open Cil_types
 
 val unreachable_proved : int ref
 val unreachable_failed : int ref
+val trivial_terminates : int ref
 val set_unreachable : WpPropId.prop_id -> unit
 val set_trivially_terminates : WpPropId.prop_id -> unit