From bc44516de11a95accd94c424b1669354872438d7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 11 May 2020 16:21:02 +0200
Subject: [PATCH] [wp] Visit each definition with a fresh set of visited terms
Fixes BTS 2501
---
src/plugins/wp/Definitions.ml | 17 +++++++++++-----
src/plugins/wp/tests/wp_bts/bts_2501.i | 14 +++++++++++++
.../tests/wp_bts/oracle/bts_2501.res.oracle | 20 +++++++++++++++++++
3 files changed, 46 insertions(+), 5 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_bts/bts_2501.i
create mode 100644 src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index e20c9582fe1..6a55329e78d 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -404,12 +404,19 @@ class virtual visitor main =
| Inductive cases -> List.iter (fun l -> self#vdlemma l) cases
method private vdfun d =
+ let old_terms = terms in
+ terms <- Tset.empty ;
begin
- List.iter self#vparam d.d_params ;
- self#vdefinition d.d_definition ;
- self#vproperties d.d_definition ;
- self#on_dfun d ;
- end
+ try
+ List.iter self#vparam d.d_params ;
+ self#vdefinition d.d_definition ;
+ self#vproperties d.d_definition ;
+ self#on_dfun d ;
+ with e ->
+ terms <- old_terms ;
+ raise e
+ end ;
+ terms <- old_terms
method private vlfun f =
match Symbol.find f with
diff --git a/src/plugins/wp/tests/wp_bts/bts_2501.i b/src/plugins/wp/tests/wp_bts/bts_2501.i
new file mode 100644
index 00000000000..442e1d8f59e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/bts_2501.i
@@ -0,0 +1,14 @@
+/* run.config
+ OPT:-wp-gen -wp-prover why3
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+/*@
+ logic integer F(integer m) = (m <= 0) ? 0 : F(m) ;
+ logic integer R(integer p) = (p < 0) ? -1 : R(p-1) + F(R(p-1));
+
+ lemma R_1: \forall integer p; R(p) == R(p-1) + F(R(p-1));
+ lemma R_2: \forall integer p; 0 <= R(p);
+*/
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
new file mode 100644
index 00000000000..f38cfc4e5fd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/bts_2501.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 2 goals scheduled
+[wp] 2 goals generated
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Lemma R_1:
+Prove: let x_0 = (L_R (p_0-1)) in (x_0+(L_F x_0))=(L_R p_0)
+
+------------------------------------------------------------
+
+Lemma R_2:
+Assume: 'R_1'
+Prove: 0<=(L_R p_0)
+
+------------------------------------------------------------
--
GitLab