From 133a630a71a9ab7d045569376f94f1d752e3f08c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 10 Dec 2020 15:46:25 +0100
Subject: [PATCH] [wp] Do not look for closed terms in model lookup

---
 src/plugins/wp/MemVar.ml                        |  6 +++++-
 src/plugins/wp/tests/wp_hoare/model_lookup.i    | 14 ++++++++++++++
 .../wp_hoare/oracle/model_lookup.res.oracle     | 17 +++++++++++++++++
 .../wp_tip/oracle/chunk_printing.res.oracle     |  4 ++--
 4 files changed, 38 insertions(+), 3 deletions(-)
 create mode 100644 src/plugins/wp/tests/wp_hoare/model_lookup.i
 create mode 100644 src/plugins/wp/tests/wp_hoare/oracle/model_lookup.res.oracle

diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 6706a5a6f19..a718b831252 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -453,7 +453,11 @@ struct
     | Iinit _ -> Sigs.Mlval (ilval c, KInit)
 
   let lookup s e =
-    try imval (Tmap.find e s.svar)
+    try
+      (* If the term is closed, any variable simplified to [e] can match. Thus,
+         we could return a variable that equals to [e] but is not really [e]. *)
+      if Lang.F.is_closed e then Sigs.Mterm
+      else imval (Tmap.find e s.svar)
     with Not_found -> M.lookup s.smem e
 
   let apply f s =
diff --git a/src/plugins/wp/tests/wp_hoare/model_lookup.i b/src/plugins/wp/tests/wp_hoare/model_lookup.i
new file mode 100644
index 00000000000..ab8f168e9fa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/model_lookup.i
@@ -0,0 +1,14 @@
+/* run.config
+   OPT: -wp-prop C
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+void foo(int y){
+  int x ;
+  // This assertion SHALL BE VISIBLE in the VC generated for C
+  //@ assert 0 <= y <= 4 ==> \false ;
+  x = 1 ;
+  //@ check C: x == y ;
+}
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/model_lookup.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/model_lookup.res.oracle
new file mode 100644
index 00000000000..21c6e1bbce7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle/model_lookup.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_hoare/model_lookup.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Check 'C' (file tests/wp_hoare/model_lookup.i, line 13):
+Assume {
+  Type: is_sint32(y).
+  (* Assertion *)
+  Have: ((0 <= y) -> ((y <= 4) -> false)).
+}
+Prove: y = 1.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index 598ec02c22b..091d995adcd 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -17,10 +17,10 @@ Assume {
   Stmt { L1:  }
   Stmt { x.a = `v;  }
   (* Call 'get_int' *)
-  Have: ((x@L1.F1_V_a) = `v) \/ (« y->a »@L1 = `v).
+  Have: ((x@L1.F1_V_a) = `v) \/ (« null->a »@L1 = `v).
   Stmt { x.b = `v_1;  }
   (* Call 'get_uint' *)
-  Have: ((x@L1.F1_V_b) = `v_1) \/ (« y->b »@L1 = `v_1).
+  Have: ((x@L1.F1_V_b) = `v_1) \/ (« null->b »@L1 = `v_1).
 }
 Prove: `x_2 = `x_1.
 
-- 
GitLab