From 2a731e07f35c26a93e25ea17486ef82bdf84eb32 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 7 Apr 2020 15:31:12 +0200
Subject: [PATCH] [wp] Initialized range on Ref is assumed in MemVar
---
src/plugins/wp/MemVar.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 854010dbff5..a693fa73f0b 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1067,7 +1067,7 @@ struct
end
| Rrange(l,elt, Some a, Some b) ->
begin match l with
- | Ref x -> noref ~op:"initialized sub-range of" x
+ | Ref _ -> p_true
| Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
| Val(m,x,p) ->
try
--
GitLab