[wp] more tests for issue 751

src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle

@@ -56,3 +56,310 @@ Assume {
 Prove: j <= 7.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function issue_751
+------------------------------------------------------------
+
+Goal Check (file tests/wp_bts/issue_751.i, line 32):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_bts/issue_751.i, line 33):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_bts/issue_751.i, line 34):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_bts/issue_751.i, line 35):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 37)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Assume { Type: is_sint32(V). (* Goal *) When: 0 <= V. }
+Prove: ((-3) <= V) <-> ((-4) <= V).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Assume { Type: is_sint32(V). (* Goal *) When: 0 < V. }
+Prove: (V <= (-3)) <-> (V <= (-4)).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Assume { Type: is_sint32(V). (* Goal *) When: 0 < V. }
+Prove: ((-2) <= V) <-> ((-3) <= V).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Assume { Type: is_sint32(V). (* Goal *) When: 0 <= V. }
+Prove: (V <= (-4)) <-> (V <= (-5)).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 38)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: V <= 0.
+  (* Call 'checks' *)
+  Have: (((0 <= V) -> (((-3) <= V) <-> ((-4) <= V)))) /\
+      (((0 <= V) -> ((V <= (-4)) <-> (V <= (-5))))).
+}
+Prove: (V <= 113) <-> (V <= 95).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: V <= 0.
+  (* Call 'checks' *)
+  Have: (((0 <= V) -> (((-3) <= V) <-> ((-4) <= V)))) /\
+      (((0 <= V) -> ((V <= (-4)) <-> (V <= (-5))))).
+}
+Prove: (95 <= V) <-> (77 <= V).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: V <= 0.
+  (* Call 'checks' *)
+  Have: (((0 <= V) -> (((-3) <= V) <-> ((-4) <= V)))) /\
+      (((0 <= V) -> ((V <= (-4)) <-> (V <= (-5))))).
+}
+Prove: (V <= 94) <-> (V <= 76).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 40)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: V <= 0.
+  (* Call 'checks' *)
+  Have: (((0 <= V) -> (((-3) <= V) <-> ((-4) <= V)))) /\
+      (((0 <= V) -> ((V <= (-4)) <-> (V <= (-5))))).
+}
+Prove: (114 <= V) <-> (96 <= V).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: 0 <= V.
+  (* Call 'checks' *)
+  Have: (((-3) <= V) <-> ((-4) <= V)) /\ ((V <= (-4)) <-> (V <= (-5))) /\
+      (((0 < V) -> (((-2) <= V) <-> ((-3) <= V)))) /\
+      (((0 < V) -> ((V <= (-3)) <-> (V <= (-4))))).
+  (* Call 'checks' *)
+  Have: (((V <= 0) -> ((95 <= V) <-> (77 <= V)))) /\
+      (((V <= 0) -> ((114 <= V) <-> (96 <= V)))) /\
+      (((V <= 0) -> ((V <= 94) <-> (V <= 76)))) /\
+      (((V <= 0) -> ((V <= 113) <-> (V <= 95)))).
+}
+Prove: (V <= (-139)) <-> (V <= (-161)).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: 0 <= V.
+  (* Call 'checks' *)
+  Have: (((-3) <= V) <-> ((-4) <= V)) /\ ((V <= (-4)) <-> (V <= (-5))) /\
+      (((0 < V) -> (((-2) <= V) <-> ((-3) <= V)))) /\
+      (((0 < V) -> ((V <= (-3)) <-> (V <= (-4))))).
+  (* Call 'checks' *)
+  Have: (((V <= 0) -> ((95 <= V) <-> (77 <= V)))) /\
+      (((V <= 0) -> ((114 <= V) <-> (96 <= V)))) /\
+      (((V <= 0) -> ((V <= 94) <-> (V <= 76)))) /\
+      (((V <= 0) -> ((V <= 113) <-> (V <= 95)))).
+}
+Prove: ((-161) <= V) <-> ((-183) <= V).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: 0 <= V.
+  (* Call 'checks' *)
+  Have: (((-3) <= V) <-> ((-4) <= V)) /\ ((V <= (-4)) <-> (V <= (-5))) /\
+      (((0 < V) -> (((-2) <= V) <-> ((-3) <= V)))) /\
+      (((0 < V) -> ((V <= (-3)) <-> (V <= (-4))))).
+  (* Call 'checks' *)
+  Have: (((V <= 0) -> ((95 <= V) <-> (77 <= V)))) /\
+      (((V <= 0) -> ((114 <= V) <-> (96 <= V)))) /\
+      (((V <= 0) -> ((V <= 94) <-> (V <= 76)))) /\
+      (((V <= 0) -> ((V <= 113) <-> (V <= 95)))).
+}
+Prove: (V <= (-162)) <-> (V <= (-184)).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_max' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_pos_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Assume {
+  Type: is_sint32(V).
+  (* Goal *)
+  When: 0 <= V.
+  (* Call 'checks' *)
+  Have: (((-3) <= V) <-> ((-4) <= V)) /\ ((V <= (-4)) <-> (V <= (-5))) /\
+      (((0 < V) -> (((-2) <= V) <-> ((-3) <= V)))) /\
+      (((0 < V) -> ((V <= (-3)) <-> (V <= (-4))))).
+  (* Call 'checks' *)
+  Have: (((V <= 0) -> ((95 <= V) <-> (77 <= V)))) /\
+      (((V <= 0) -> ((114 <= V) <-> (96 <= V)))) /\
+      (((V <= 0) -> ((V <= 94) <-> (V <= 76)))) /\
+      (((V <= 0) -> ((V <= 113) <-> (V <= 95)))).
+}
+Prove: ((-138) <= V) <-> ((-160) <= V).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'strict_neg_min' in 'checks'' in 'issue_751' at call 'checks' (file tests/wp_bts/issue_751.i, line 41)
+:
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle

@@ -3,15 +3,52 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
-[wp] 4 goals scheduled
+[wp] 40 goals scheduled
 [wp] [Alt-Ergo 2.0.0] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
 [wp] [Qed] Goal typed_acquire_loop_invariant_RANGE_established : Valid
 [wp] [Qed] Goal typed_acquire_loop_assigns_part1 : Valid
 [wp] [Alt-Ergo 2.0.0] Goal typed_acquire_loop_assigns_part2 : Valid
-[wp] Proved goals:    4 / 4
-  Qed:               2 
-  Alt-Ergo 2.0.0:    2
+[wp] [Qed] Goal typed_issue_751_check : Valid
+[wp] [Qed] Goal typed_issue_751_check_2 : Valid
+[wp] [Qed] Goal typed_issue_751_check_3 : Valid
+[wp] [Qed] Goal typed_issue_751_check_4 : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_pos_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_neg_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_pos_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_neg_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_strict_pos_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_strict_neg_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_strict_pos_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_requires_strict_neg_min : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_2_requires_pos_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_2_requires_neg_max : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_2_requires_pos_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_2_requires_neg_min : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_2_requires_strict_pos_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_2_requires_strict_neg_max : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_2_requires_strict_pos_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_2_requires_strict_neg_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_3_requires_pos_max : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_3_requires_neg_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_3_requires_pos_min : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_3_requires_neg_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_3_requires_strict_pos_max : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_3_requires_strict_neg_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_3_requires_strict_pos_min : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_3_requires_strict_neg_min : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_4_requires_pos_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_4_requires_neg_max : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_4_requires_pos_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_4_requires_neg_min : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_4_requires_strict_pos_max : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_4_requires_strict_neg_max : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_issue_751_call_checks_4_requires_strict_pos_min : Valid
+[wp] [Qed] Goal typed_issue_751_call_checks_4_requires_strict_neg_min : Valid
+[wp] Proved goals:   40 / 40
+  Qed:              26 
+  Alt-Ergo 2.0.0:   14
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   acquire                   2        2        4       100%
+  issue_751                24       12       36       100%
 ------------------------------------------------------------