From 8de4abbc2ed966355fbcd4d479734d13538f7685 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 26 Jun 2019 09:22:59 +0200
Subject: [PATCH] [wp] set add bonus into Cint simplifier as it should be
---
src/plugins/wp/Cint.ml | 3 +-
.../frama_c_exo1_solved.res.oracle | 4 +-
.../wp_typed/oracle/user_init.0.res.oracle | 70 ++++++++-----------
.../wp_typed/oracle/user_init.1.res.oracle | 70 ++++++++-----------
4 files changed, 66 insertions(+), 81 deletions(-)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 44615afda69..2772546a63e 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -836,7 +836,8 @@ let reduce_bound v tv dom t : term =
with Exc.Unknown i -> i in
(** we try to reduce the bounds of the domains, when trivially false *)
let dom_red = Ival.inject_range (Some min_bound) (Some max_bound) in
- if not (Ival.equal dom_red dom) && Ival.is_included dom_red dom
+ assert ( Ival.is_included dom_red dom);
+ if Ival.equal dom_red dom
then t
else
(e_imply [e_leq (e_zint min_bound) tv;
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
index d7e1a7f9702..04777edf3a4 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
@@ -21,7 +21,7 @@
[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-exo1 6 4 (176..200) 10 100%
+exo1 6 4 (176..224) 10 100%
-------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function exo1
@@ -48,5 +48,5 @@ exo1 6 4 (176..200) 10 100%
[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-exo1 6 9 (176..200) 15 100%
+exo1 6 9 (176..224) 15 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 7c9323b15bd..466000394e6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -367,15 +367,13 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))).
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -423,8 +421,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: i <= 9.
Have: 0 <= i_1.
+ Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -458,8 +456,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: i <= 9.
Have: 0 <= i_1.
+ Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -1051,15 +1049,13 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -1092,15 +1088,13 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -1142,15 +1136,13 @@ Assume {
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -1202,8 +1194,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: i <= 9.
Have: 0 <= i_1.
+ Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index b48ff1d096a..d91b34a47a4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -367,15 +367,13 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))).
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -423,8 +421,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: i <= 9.
Have: 0 <= i_1.
+ Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -458,8 +456,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: i <= 9.
Have: 0 <= i_1.
+ Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -1051,15 +1049,13 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -1092,15 +1088,13 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -1142,15 +1136,13 @@ Assume {
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) -> false)))))))) \/
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
- ((i_4 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
- (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19)))))))))).
+Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
@@ -1202,8 +1194,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: i <= 9.
Have: 0 <= i_1.
+ Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
--
GitLab