From bd64db77f47aef1c0ee3c8f0c46b1defc6692d95 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 15 Jun 2021 15:09:09 +0200
Subject: [PATCH] [wp] Safer initialized MemVal (useless though)
---
src/plugins/wp/MemVal.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
index 950f0518a5d..bd41cf7b7c9 100644
--- a/src/plugins/wp/MemVal.ml
+++ b/src/plugins/wp/MemVal.ml
@@ -564,7 +564,8 @@ struct
| _ -> load_loc ~assume:false sigma obj l
end
- let load_init _sigma _obj _loc = e_false
+ let load_init _sigma obj _loc =
+ e_var @@ Lang.freshvar ~basename:"i" @@ Lang.init_of_object obj
(* -------------------------------------------------------------------------- *)
(* --- Memory Store --- *)
--
GitLab