[wp] Add terminates variant test

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

@@ -2,6 +2,64 @@
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function f1
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 34) in 'f1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Assume {
+  Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+  (* Residual *)
+  When: c1_0 != 0.
+  (* Goal *)
+  When: 0 <= c1_0.
+  (* Invariant *)
+  Have: (cpt_0 <= c1_0) /\ (0 <= cpt_0).
+  (* Else *)
+  Have: 2 <= cpt_0.
+}
+Prove: (0 < cpt_0) /\ (cpt_0 <= (1 + c1_0)).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/terminates_variant_option.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Assume {
+  Type: is_sint32(cpt_0).
+  (* Invariant *)
+  Have: (cpt_0 <= 0) /\ (0 <= cpt_0).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Assume {
+  Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+  (* Residual *)
+  When: c1_0 != 0.
+  (* Invariant *)
+  Have: ((0 <= c1_0) -> ((cpt_0 <= c1_0) /\ (0 <= cpt_0))).
+  (* Else *)
+  Have: 2 <= cpt_0.
+}
+Prove: 0 <= cpt_0.
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Function fails_decreases
 ------------------------------------------------------------

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

@@ -2,6 +2,59 @@
 [kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function f1
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 34) in 'f1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Assume {
+  Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+  (* Residual *)
+  When: c1_0 != 0.
+  (* Goal *)
+  When: 0 <= c1_0.
+  (* Invariant *)
+  Have: (cpt_0 <= c1_0) /\ (0 <= cpt_0).
+  (* Else *)
+  Have: 2 <= cpt_0.
+}
+Prove: (0 < cpt_0) /\ (cpt_0 <= (1 + c1_0)).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/terminates_variant_option.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Assume {
+  Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+  (* Goal *)
+  When: c1_0 != 0.
+  (* Invariant *)
+  Have: ((0 <= c1_0) -> ((cpt_0 <= c1_0) /\ (0 <= cpt_0))).
+  (* Else *)
+  Have: 2 <= cpt_0.
+}
+Prove: 0 <= cpt_0.
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Function fails_decreases
 ------------------------------------------------------------

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] 11 goals scheduled
+[wp] 17 goals scheduled
 [wp] [Qed] Goal typed_fails_positive_terminates : Valid
 [wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
 [wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
@@ -14,11 +14,18 @@
 [wp] [Qed] Goal typed_fails_decreases_loop_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_fails_decreases_loop_variant_decrease : Unsuccess
 [wp] [Qed] Goal typed_fails_decreases_loop_variant_positive : Valid
-[wp] Proved goals:    9 / 11
-  Qed:             8 
-  Alt-Ergo:        1  (unsuccess: 2)
+[wp] [Qed] Goal typed_f1_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_f1_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
+[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:   14 / 17
+  Qed:            11 
+  Alt-Ergo:        3  (unsuccess: 3)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   fails_positive            5        1        7      85.7%
   fails_decreases           3        -        4      75.0%
+  f1                        3        2        6      83.3%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.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] 11 goals scheduled
+[wp] 17 goals scheduled
 [wp] [Qed] Goal typed_fails_positive_terminates : Valid
 [wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
 [wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
@@ -14,11 +14,18 @@
 [wp] [Qed] Goal typed_fails_decreases_loop_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_fails_decreases_loop_variant_decrease : Valid
 [wp] [Qed] Goal typed_fails_decreases_loop_variant_positive : Valid
-[wp] Proved goals:   11 / 11
-  Qed:             9 
-  Alt-Ergo:        2
+[wp] [Qed] Goal typed_f1_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_f1_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
+[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:   17 / 17
+  Qed:            13 
+  Alt-Ergo:        4
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   fails_positive            6        1        7       100%
   fails_decreases           3        1        4       100%
+  f1                        4        2        6       100%
 ------------------------------------------------------------

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

@@ -30,3 +30,18 @@ void fails_decreases(int keep_going){
     if(! keep_going) i-- ;
   }
 }
+
+//@ terminates c1 != 0;
+void f1 (int c1, int c2) {
+  int cpt = c1 ;
+  /*@ loop invariant c1 >= 0 ==> 0 <= cpt <= c1 ;
+    @ loop assigns cpt ;
+    @ loop variant cpt ;
+    @*/
+  while (1) {
+    if (c1 || c2) {
+      cpt --;
+      if (cpt <= 0) break;
+    }
+  }
+}