Skip to content
Snippets Groups Projects
Commit b19ecab8 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] fix decreases positive

parent 250a5c94
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 24 additions and 31 deletions
src/plugins/wp/cfgWP.ml
+ 1
− 1
View file @ b19ecab8
......@@ -1162,7 +1162,7 @@ struct
| (caller_d, rel), Some (callee_d,_ ) ->
let rel caller callee = match rel with
| None ->
p_and (p_leq e_zero callee) (p_lt callee caller)
p_and (p_leq e_zero caller) (p_lt callee caller)
| Some rel ->
(L.in_frame call_f (L.call_pred call_e))
rel [] [caller ; callee]
......
src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
+ 1
− 1
View file @ b19ecab8
......@@ -122,7 +122,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 12
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+ 9
− 9
View file @ b19ecab8
......@@ -24,7 +24,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 17
Assume { Type: is_uint32(n). (* Else *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -52,7 +52,7 @@ Prove: 0 < n.
Goal Recursion variant:
Call Effect at line 40
Assume { Type: is_sint32(n). (* Else *) Have: n != 0. }
Prove: 0 < n.
Prove: 0 <= n.
------------------------------------------------------------
------------------------------------------------------------
......@@ -120,7 +120,7 @@ Prove: P_Rel(n, n).
Goal Recursion variant:
Call Effect at line 55
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -130,14 +130,14 @@ Prove: to_uint32(n - 1) < n.
Goal Recursion variant (1/2):
Call Effect at line 59
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 60
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
......@@ -157,7 +157,7 @@ Prove: false.
Goal Recursion variant (2/2):
Call Effect at line 72
Assume { Type: is_uint32(n). (* Then *) Have: 31 <= n. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -179,7 +179,7 @@ Prove: to_uint32(n - 1) <= 10.
Goal Recursion variant:
Call Effect at line 86
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -200,14 +200,14 @@ Prove: true.
Goal Recursion variant (1/2):
Call Effect at line 91
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 92
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+ 8
− 15
View file @ b19ecab8
......@@ -24,7 +24,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 17
Assume { Type: is_uint32(n). (* Else *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -51,14 +51,7 @@ Prove: 0 < n.
Goal Recursion variant:
Call Effect at line 40
Assume {
Type: is_sint32(n).
(* Goal *)
When: 0 <= n.
(* Else *)
Have: n != 0.
}
Prove: 0 < n.
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
......@@ -132,7 +125,7 @@ Prove: P_Rel(n, n).
Goal Recursion variant:
Call Effect at line 55
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -142,14 +135,14 @@ Prove: to_uint32(n - 1) < n.
Goal Recursion variant (1/2):
Call Effect at line 59
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 60
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
......@@ -169,7 +162,7 @@ Prove: false.
Goal Recursion variant (2/2):
Call Effect at line 72
Assume { Type: is_uint32(n). (* Then *) Have: 31 <= n. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -191,7 +184,7 @@ Prove: to_uint32(n - 1) <= 10.
Goal Recursion variant:
Call Effect at line 86
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......@@ -218,7 +211,7 @@ Assume {
(* Then *)
Have: x != 0.
}
Prove: to_uint32(x - 1) < x.
Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+ 1
− 1
View file @ b19ecab8
......@@ -77,7 +77,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 80
Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
Prove: to_uint32(n - 1) < n.
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+ 4
− 4
View file @ b19ecab8
......@@ -20,7 +20,7 @@
[wp] [Alt-Ergo] Goal typed_fails_facto_gen_variant : Unsuccess
[wp] [Qed] Goal typed_fact_i_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fact_i_terminates_part2 : Valid
[wp] [Alt-Ergo] Goal typed_fact_i_variant : Valid
[wp] [Qed] Goal typed_fact_i_variant : Valid
[wp] [Qed] Goal typed_fails_fact_i_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_i_terminates_part2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fails_fact_i_variant : Unsuccess
......@@ -41,15 +41,15 @@
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
[wp] [Qed] Goal typed_se_variant : Valid
[wp] Proved goals: 19 / 27
Qed: 8
Alt-Ergo: 11 (unsuccess: 8)
Qed: 9
Alt-Ergo: 10 (unsuccess: 8)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fact 1 1 2 100%
fails_fact - - 1 0.0%
facto_gen - 1 1 100%
fails_facto_gen - - 1 0.0%
fact_i 1 2 3 100%
fact_i 2 1 3 100%
fails_fact_i 1 - 3 33.3%
m2 - 2 2 100%
m1 - 1 1 100%
......
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