[wp] Detect syntactically trivial variant

src/plugins/wp/cfgAnnot.ml

@@ -490,6 +490,11 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
                   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
                 in

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

@@ -137,3 +137,21 @@ Assume {
 Prove: 0 <= v.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function trivial_variant
+------------------------------------------------------------
+
+Goal Loop assigns nothing:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 54):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 54):
+Prove: false.
+
+------------------------------------------------------------

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

@@ -2,6 +2,8 @@
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_variant_option.i:52: Warning: 
+  Loop variant is always trivially verified (terminates \false)
 ------------------------------------------------------------
   Function f1
 ------------------------------------------------------------
@@ -115,3 +117,21 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_o
 Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function trivial_variant
+------------------------------------------------------------
+
+Goal Loop assigns nothing:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 54):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 54):
+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] 14 goals scheduled
+[wp] 17 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
@@ -17,12 +17,16 @@
 [wp] [Qed] Goal typed_f1_loop_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_f1_loop_variant_decrease : Unsuccess
 [wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
-[wp] Proved goals:   11 / 14
-  Qed:             8 
-  Alt-Ergo:        3  (unsuccess: 3)
+[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)
 ------------------------------------------------------------
  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%
 ------------------------------------------------------------

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

@@ -2,7 +2,9 @@
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 14 goals scheduled
+[wp] tests/wp_acsl/terminates_variant_option.i:52: Warning: 
+  Loop variant is always trivially verified (terminates \false)
+[wp] 17 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
@@ -17,12 +19,16 @@
 [wp] [Qed] Goal typed_f1_loop_assigns : Valid
 [wp] [Qed] Goal typed_f1_loop_variant_decrease : Valid
 [wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
-[wp] Proved goals:   14 / 14
-  Qed:            10 
+[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 
   Alt-Ergo:        4
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   fails_positive            5        1        6       100%
   fails_decreases           2        1        3       100%
   f1                        3        2        5       100%
+  trivial_variant           3        -        3       100%
 ------------------------------------------------------------

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

@@ -45,3 +45,11 @@ void f1 (int c1, int c2) {
     }
   }
 }
+
+//@ terminates \false ;
+void trivial_variant(void){
+  /*@ loop assigns \nothing ;
+      loop variant -1 ;
+  */
+  while(1);
+}