[wp] extended variant verification when terminates

src/plugins/wp/cfgAnnot.ml

@@ -207,7 +207,7 @@ let get_terminates kf =
   | Some p ->
       Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
 
-let get_terminates_call kf =
+let get_terminates_hyp kf =
   let to_default option =
     if option then Logic_const.ptrue else Logic_const.pfalse in
   match Annotations.terminates kf with
@@ -307,7 +307,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
           | WritesAny -> WritesAny
           | Writes froms -> Writes (normalize_froms Normal froms)
         in
-        let terminates = get_terminates_call kf in
+        let terminates = get_terminates_hyp kf in
         {
           contract_cond = List.rev !wcond ;
           contract_hpre = List.rev !whpre ;
@@ -488,15 +488,15 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
                   WpStrategy.mk_variant_properties kf stmt ca term in
                 let intro_terminates (pid, v) =
                   pid,
-                  match get_terminates kf with
-                  | Some (_,t) when Wp_parameters.TerminatesVariantHyp.get () ->
-                      if Logic_utils.is_same_predicate t Logic_const.pfalse then
-                        Wp_parameters.warning
-                          ~source:(fst term.term_loc) ~once:true
-                          "Loop variant is always trivially verified \
-                           (terminates \\false)" ;
-                      Logic_const.pimplies (t, v)
-                  | _ -> v
+                  let t = snd @@ get_terminates_hyp kf in
+                  if Wp_parameters.TerminatesVariantHyp.get () then begin
+                    if Logic_utils.is_same_predicate t Logic_const.pfalse then
+                      Wp_parameters.warning
+                        ~source:(fst term.term_loc) ~once:true
+                        "Loop variant is always trivially verified \
+                         (terminates \\false)" ;
+                    Logic_const.pimplies (t, v)
+                  end else v
                 in
                 { l with loop_terminates = None ;
                          loop_preserved =

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

@@ -155,3 +155,21 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_o
 Prove: false.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function trivial_variant_default
+------------------------------------------------------------
+
+Goal Loop assigns nothing:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: false.
+
+------------------------------------------------------------

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

@@ -4,6 +4,8 @@
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/terminates_variant_option.i:52: Warning: 
   Loop variant is always trivially verified (terminates \false)
+[wp] tests/wp_acsl/terminates_variant_option.i:59: Warning: 
+  Loop variant is always trivially verified (terminates \false)
 ------------------------------------------------------------
   Function f1
 ------------------------------------------------------------
@@ -135,3 +137,21 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_o
 Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function trivial_variant_default
+------------------------------------------------------------
+
+Goal Loop assigns nothing:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: true.
+
+------------------------------------------------------------

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

@@ -2,7 +2,7 @@
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 17 goals scheduled
+[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
 [wp] [Qed] Goal typed_fails_positive_loop_assigns_part1 : Valid
@@ -20,13 +20,17 @@
 [wp] [Qed] Goal typed_trivial_variant_loop_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_trivial_variant_loop_variant_decrease : Unsuccess
 [wp] [Alt-Ergo] Goal typed_trivial_variant_loop_variant_positive : Unsuccess
-[wp] Proved goals:   12 / 17
-  Qed:             9 
-  Alt-Ergo:        3  (unsuccess: 5)
+[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
+  Qed:            10 
+  Alt-Ergo:        3  (unsuccess: 7)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   fails_positive            4        1        6      83.3%
   fails_decreases           2        -        3      66.7%
   f1                        2        2        5      80.0%
   trivial_variant           1        -        3      33.3%
+  trivial_variant_default   1        -        3      33.3%
 ------------------------------------------------------------

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

@@ -4,7 +4,9 @@
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/terminates_variant_option.i:52: Warning: 
   Loop variant is always trivially verified (terminates \false)
-[wp] 17 goals scheduled
+[wp] tests/wp_acsl/terminates_variant_option.i:59: Warning: 
+  Loop variant is always trivially verified (terminates \false)
+[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
 [wp] [Qed] Goal typed_fails_positive_loop_assigns_part1 : Valid
@@ -22,8 +24,11 @@
 [wp] [Qed] Goal typed_trivial_variant_loop_assigns : Valid
 [wp] [Qed] Goal typed_trivial_variant_loop_variant_decrease : Valid
 [wp] [Qed] Goal typed_trivial_variant_loop_variant_positive : Valid
-[wp] Proved goals:   17 / 17
-  Qed:            13 
+[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
+  Qed:            16 
   Alt-Ergo:        4
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
@@ -31,4 +36,5 @@
   fails_decreases           2        1        3       100%
   f1                        3        2        5       100%
   trivial_variant           3        -        3       100%
+  trivial_variant_default   3        -        3       100%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/terminates_variant_option.i

@@ -53,3 +53,10 @@ void trivial_variant(void){
   */
   while(1);
 }
+
+void trivial_variant_default(void){
+  /*@ loop assigns \nothing ;
+      loop variant -1 ;
+  */
+  while(1);
+}