From 75e0e38a438601fe07b2627e97f0faec6a434010 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 11 Dec 2020 11:29:31 +0100
Subject: [PATCH] [wp] Lookup only ignores primitive terms
---
src/plugins/wp/Conditions.ml | 8 +++++---
src/plugins/wp/MemVar.ml | 6 +-----
.../wp/tests/wp_tip/oracle/chunk_printing.res.oracle | 4 ++--
3 files changed, 8 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index d6e531f56be..1ff6550e705 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1595,9 +1595,11 @@ struct
let visited = ref Tset.empty in
let rec term_is_init_in_states states t =
let raise_if_is_init t s =
- match Mstate.lookup s t with
- | Mlval(_, KInit) | Mchunk(_, KInit) -> raise Found
- | _ -> ()
+ if Lang.F.is_primitive t then ()
+ else
+ match Mstate.lookup s t with
+ | Mlval(_, KInit) | Mchunk(_, KInit) -> raise Found
+ | _ -> ()
in
if Tset.mem t !visited then ()
else begin
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index a718b831252..6706a5a6f19 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -453,11 +453,7 @@ struct
| Iinit _ -> Sigs.Mlval (ilval c, KInit)
let lookup s e =
- 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)
+ try 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_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index 091d995adcd..598ec02c22b 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) \/ (« null->a »@L1 = `v).
+ Have: ((x@L1.F1_V_a) = `v) \/ (« y->a »@L1 = `v).
Stmt { x.b = `v_1; }
(* Call 'get_uint' *)
- Have: ((x@L1.F1_V_b) = `v_1) \/ (« null->b »@L1 = `v_1).
+ Have: ((x@L1.F1_V_b) = `v_1) \/ (« y->b »@L1 = `v_1).
}
Prove: `x_2 = `x_1.
--
GitLab