Skip to content
Snippets Groups Projects
Commit 6510c2bd authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] replaces lc_open,lc_iter,lc_map by e_open,f_iter,f_map into Cint simplifier (oracle changes)

parent 583cf432
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
+ 2
− 2
View file @ 6510c2bd
...@@ -204,7 +204,7 @@ Assume { ...@@ -204,7 +204,7 @@ Assume {
Have: (0 <= i) /\ (i <= j) /\ (j <= 19). Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Exit Effects *) (* Exit Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> 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. Prove: i <= 0.
...@@ -220,7 +220,7 @@ Assume { ...@@ -220,7 +220,7 @@ Assume {
Have: (0 <= i) /\ (i <= j) /\ (j <= 19). Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Call Effects *) (* Call Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> 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. Prove: i <= 0.
......
src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+ 43
− 35
View file @ 6510c2bd
...@@ -367,13 +367,15 @@ Assume { ...@@ -367,13 +367,15 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20) (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))). [shift_sint32(a_1, i_3)] = v))).
} }
Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -421,8 +423,8 @@ Assume {
Have: i_2 <= 9. Have: i_2 <= 9.
Have: i_3 <= 19. Have: i_3 <= 19.
Have: 0 <= i. Have: 0 <= i.
Have: 0 <= i_1.
Have: i <= 9. Have: i <= 9.
Have: 0 <= i_1.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -456,8 +458,8 @@ Assume { ...@@ -456,8 +458,8 @@ Assume {
Have: i_2 <= 9. Have: i_2 <= 9.
Have: i_3 <= 19. Have: i_3 <= 19.
Have: 0 <= i. Have: 0 <= i.
Have: 0 <= i_1.
Have: i <= 9. Have: i <= 9.
Have: 0 <= i_1.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -1049,13 +1051,15 @@ Assume { ...@@ -1049,13 +1051,15 @@ Assume {
(* Invariant 'Partial_j' *) (* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))). 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) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -1088,13 +1092,15 @@ Assume {
(* Invariant 'Partial_j' *) (* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))). 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) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -1136,13 +1142,15 @@ Assume {
(* Then *) (* Then *)
Have: j <= 19. Have: j <= 19.
} }
Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -1175,8 +1183,8 @@ Assume {
(* Invariant 'Range_j' *) (* Invariant 'Range_j' *)
Have: j <= 20. Have: j <= 20.
} }
Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\ Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
(i <= i_2) /\ (0 <= i_1) /\ (j <= i_1) /\ (i_2 <= 9) /\ (i_1 <= 19). (0 <= i_1) /\ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1194,8 +1202,8 @@ Assume { ...@@ -1194,8 +1202,8 @@ Assume {
Have: i_2 <= 9. Have: i_2 <= 9.
Have: i_3 <= 19. Have: i_3 <= 19.
Have: 0 <= i. Have: 0 <= i.
Have: 0 <= i_1.
Have: i <= 9. Have: i <= 9.
Have: 0 <= i_1.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone_i' *) (* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) -> Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
...@@ -1642,8 +1650,8 @@ Assume { ...@@ -1642,8 +1650,8 @@ Assume {
(* Invariant 'Range_j' *) (* Invariant 'Range_j' *)
Have: j <= 20. Have: j <= 20.
} }
Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\ Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
(i <= i_2) /\ (j <= i_1) /\ (i_2 <= 9). (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9).
------------------------------------------------------------ ------------------------------------------------------------
......
src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+ 43
− 35
View file @ 6510c2bd
...@@ -367,13 +367,15 @@ Assume { ...@@ -367,13 +367,15 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20) (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))). [shift_sint32(a_1, i_3)] = v))).
} }
Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -421,8 +423,8 @@ Assume {
Have: i_2 <= 9. Have: i_2 <= 9.
Have: i_3 <= 19. Have: i_3 <= 19.
Have: 0 <= i. Have: 0 <= i.
Have: 0 <= i_1.
Have: i <= 9. Have: i <= 9.
Have: 0 <= i_1.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -456,8 +458,8 @@ Assume { ...@@ -456,8 +458,8 @@ Assume {
Have: i_2 <= 9. Have: i_2 <= 9.
Have: i_3 <= 19. Have: i_3 <= 19.
Have: 0 <= i. Have: 0 <= i.
Have: 0 <= i_1.
Have: i <= 9. Have: i <= 9.
Have: 0 <= i_1.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -1049,13 +1051,15 @@ Assume { ...@@ -1049,13 +1051,15 @@ Assume {
(* Invariant 'Partial_j' *) (* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))). 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) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -1088,13 +1092,15 @@ Assume {
(* Invariant 'Partial_j' *) (* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))). 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) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -1136,13 +1142,15 @@ Assume {
(* Then *) (* Then *)
Have: j <= 19. Have: j <= 19.
} }
Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
((i_3 <= 19) -> false))))) \/ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) -> ((i_4 <= 19) -> false)))))))) \/
((i_3 <= 19) -> (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
(exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
(i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\ ((i_4 <= 19) ->
(i_5 <= 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 { ...@@ -1175,8 +1183,8 @@ Assume {
(* Invariant 'Range_j' *) (* Invariant 'Range_j' *)
Have: j <= 20. Have: j <= 20.
} }
Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\ Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
(i <= i_2) /\ (0 <= i_1) /\ (j <= i_1) /\ (i_2 <= 9) /\ (i_1 <= 19). (0 <= i_1) /\ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1194,8 +1202,8 @@ Assume { ...@@ -1194,8 +1202,8 @@ Assume {
Have: i_2 <= 9. Have: i_2 <= 9.
Have: i_3 <= 19. Have: i_3 <= 19.
Have: 0 <= i. Have: 0 <= i.
Have: 0 <= i_1.
Have: i <= 9. Have: i <= 9.
Have: 0 <= i_1.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone_i' *) (* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) -> Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
...@@ -1642,8 +1650,8 @@ Assume { ...@@ -1642,8 +1650,8 @@ Assume {
(* Invariant 'Range_j' *) (* Invariant 'Range_j' *)
Have: j <= 20. Have: j <= 20.
} }
Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\ Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
(i <= i_2) /\ (j <= i_1) /\ (i_2 <= 9). (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9).
------------------------------------------------------------ ------------------------------------------------------------
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment