From 7d8c60d71cb15e1c71306a10be8f1446226c4e07 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 10 Feb 2020 14:39:02 +0100
Subject: [PATCH] [wp] more tests for issue 751
---
.../tests/wp_bts/oracle/issue_751.res.oracle | 307 ++++++++++++++++++
.../wp_bts/oracle_qualif/issue_751.res.oracle | 45 ++-
2 files changed, 348 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index 9940170f093..6e440e1cd4f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/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.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
index 55dd8352961..efa8250b27b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+++ b/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%
------------------------------------------------------------
--
GitLab