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

[wp] set add bonus into Cint simplifier as it should be

parent 6510c2bd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/Cint.ml
+ 2
− 1
View file @ 8de4abbc
...@@ -836,7 +836,8 @@ let reduce_bound v tv dom t : term = ...@@ -836,7 +836,8 @@ let reduce_bound v tv dom t : term =
with Exc.Unknown i -> i in with Exc.Unknown i -> i in
(** we try to reduce the bounds of the domains, when trivially false *) (** 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 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 then t
else else
(e_imply [e_leq (e_zint min_bound) tv; (e_imply [e_leq (e_zint min_bound) tv;
......
src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+ 2
− 2
View file @ 8de4abbc
...@@ -21,7 +21,7 @@ ...@@ -21,7 +21,7 @@
[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json' [wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
exo1 6 4 (176..200) 10 100% exo1 6 4 (176..224) 10 100%
------------------------------------------------------------- -------------------------------------------------------------
[wp] Running WP plugin... [wp] Running WP plugin...
[rte] annotating function exo1 [rte] annotating function exo1
...@@ -48,5 +48,5 @@ exo1 6 4 (176..200) 10 100% ...@@ -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' [wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
exo1 6 9 (176..200) 15 100% exo1 6 9 (176..224) 15 100%
------------------------------------------------------------- -------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+ 31
− 39
View file @ 8de4abbc
...@@ -367,15 +367,13 @@ Assume { ...@@ -367,15 +367,13 @@ 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_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -423,8 +421,8 @@ Assume { ...@@ -423,8 +421,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: i <= 9.
Have: 0 <= i_1. Have: 0 <= i_1.
Have: i <= 9.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -458,8 +456,8 @@ Assume { ...@@ -458,8 +456,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: i <= 9.
Have: 0 <= i_1. Have: 0 <= i_1.
Have: i <= 9.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -1051,15 +1049,13 @@ Assume { ...@@ -1051,15 +1049,13 @@ 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_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1092,15 +1088,13 @@ Assume { ...@@ -1092,15 +1088,13 @@ 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_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1142,15 +1136,13 @@ Assume { ...@@ -1142,15 +1136,13 @@ Assume {
(* Then *) (* Then *)
Have: j <= 19. Have: j <= 19.
} }
Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1202,8 +1194,8 @@ Assume { ...@@ -1202,8 +1194,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: i <= 9.
Have: 0 <= i_1. Have: 0 <= i_1.
Have: i <= 9.
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) ->
......
src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+ 31
− 39
View file @ 8de4abbc
...@@ -367,15 +367,13 @@ Assume { ...@@ -367,15 +367,13 @@ 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_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -423,8 +421,8 @@ Assume { ...@@ -423,8 +421,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: i <= 9.
Have: 0 <= i_1. Have: 0 <= i_1.
Have: i <= 9.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -458,8 +456,8 @@ Assume { ...@@ -458,8 +456,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: i <= 9.
Have: 0 <= i_1. Have: 0 <= i_1.
Have: i <= 9.
Have: i_1 <= 19. Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *) (* Loop assigns 'lack,Zone' *)
Have: forall a : addr. Have: forall a : addr.
...@@ -1051,15 +1049,13 @@ Assume { ...@@ -1051,15 +1049,13 @@ 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_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1092,15 +1088,13 @@ Assume { ...@@ -1092,15 +1088,13 @@ 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_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1142,15 +1136,13 @@ Assume { ...@@ -1142,15 +1136,13 @@ Assume {
(* Then *) (* Then *)
Have: j <= 19. Have: j <= 19.
} }
Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> ((i_3 <= 19) -> false))))) \/
((i_4 <= 19) -> false)))))))) \/ (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((i_3 <= 19) ->
(forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) -> (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
((i_4 <= 19) -> (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
(exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\ (i_5 <= 19))))))).
(i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
(i_5 <= 19)))))))))).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -1202,8 +1194,8 @@ Assume { ...@@ -1202,8 +1194,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: i <= 9.
Have: 0 <= i_1. Have: 0 <= i_1.
Have: i <= 9.
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) ->
......
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