From 6510c2bd25340321225e57fed910a56d1cbab112 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 26 Jun 2019 08:25:52 +0200
Subject: [PATCH] [wp] replaces lc_open,lc_iter,lc_map by e_open,f_iter,f_map
into Cint simplifier (oracle changes)
---
.../wp_acsl/oracle/assigns_range.res.oracle | 4 +-
.../wp_typed/oracle/user_init.0.res.oracle | 78 ++++++++++---------
.../wp_typed/oracle/user_init.1.res.oracle | 78 ++++++++++---------
3 files changed, 88 insertions(+), 72 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
index dc175209d04..049b05cc6d2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
@@ -204,7 +204,7 @@ Assume {
Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Exit Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((j < i_1) \/ (i_1 < 0)) -> (t4_0[i_1] = t4_1[i_1])))).
+ (((i_1 < 0) \/ (j < i_1)) -> (t4_0[i_1] = t4_1[i_1])))).
}
Prove: i <= 0.
@@ -220,7 +220,7 @@ Assume {
Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Call Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((j < i_1) \/ (i_1 < 0)) -> (t4_0[i_1] = t4_1[i_1])))).
+ (((i_1 < 0) \/ (j < i_1)) -> (t4_0[i_1] = t4_1[i_1])))).
}
Prove: i <= 0.
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 fe5efd3387b..7c9323b15bd 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,13 +367,15 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))).
}
-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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -421,8 +423,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -456,8 +458,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -1049,13 +1051,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -1088,13 +1092,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -1136,13 +1142,15 @@ Assume {
(* Then *)
Have: j <= 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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -1175,8 +1183,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (0 <= i_1) /\ (j <= i_1) /\ (i_2 <= 9) /\ (i_1 <= 19).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (0 <= i_1) /\ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------
@@ -1194,8 +1202,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
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) ->
@@ -1642,8 +1650,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (j <= i_1) /\ (i_2 <= 9).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 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 39da789135d..b48ff1d096a 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,13 +367,15 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))).
}
-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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -421,8 +423,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -456,8 +458,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -1049,13 +1051,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -1088,13 +1092,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -1136,13 +1142,15 @@ Assume {
(* Then *)
Have: j <= 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))))))).
+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)))))))))).
------------------------------------------------------------
@@ -1175,8 +1183,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (0 <= i_1) /\ (j <= i_1) /\ (i_2 <= 9) /\ (i_1 <= 19).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (0 <= i_1) /\ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------
@@ -1194,8 +1202,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
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) ->
@@ -1642,8 +1650,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (j <= i_1) /\ (i_2 <= 9).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9).
------------------------------------------------------------
--
GitLab