From b19ecab808f7bbfdc92d126453fb9fa68bc3ce93 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 27 Apr 2022 08:26:27 +0200
Subject: [PATCH] [wp] fix decreases positive
---
src/plugins/wp/cfgWP.ml | 2 +-
.../tests/wp_acsl/oracle/clusters.res.oracle | 2 +-
.../wp_acsl/oracle/decreases.0.res.oracle | 18 +++++++--------
.../wp_acsl/oracle/decreases.1.res.oracle | 23 +++++++------------
.../oracle/terminates_formulae.res.oracle | 2 +-
.../oracle_qualif/decreases.1.res.oracle | 8 +++----
6 files changed, 24 insertions(+), 31 deletions(-)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ee6d749805a..110ef26efae 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -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]
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
index 61a3435b5bb..65805aa212d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
@@ -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).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
index d20b0623277..84ff1f41b85 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
@@ -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).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
index acfb72158d9..f45e5a772fe 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
@@ -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).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index d8eeb1c7538..484dd6e31ec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -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).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
index 541e824ca01..f18fe8e1bdf 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
@@ -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%
--
GitLab