From bb481ec288b03c3ed9c8fbe5809478bb21671a26 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 10 Apr 2020 09:21:13 +0200
Subject: [PATCH] [wp] MemVar initialized fixes issue with typing + havoc some
variables
---
src/plugins/wp/Lang.ml | 7 ++++++-
src/plugins/wp/MemVar.ml | 4 ++++
2 files changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2882e2aa095..bd903ad3f34 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -168,6 +168,10 @@ let sort_of_object = function
| C_float _ -> Logic.Sreal
| C_pointer _ | C_comp _ | C_array _ -> Logic.Sdata
+let init_sort_of_object = function
+ | C_int _ | C_float _ | C_pointer _ -> Logic.Sbool
+ | C_comp _ | C_array _ -> Logic.Sdata
+
let sort_of_ctype t = sort_of_object (Ctypes.object_of t)
let sort_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with
@@ -402,7 +406,8 @@ struct
let sort = function
| Mfield(_,_,_,s) -> Qed.Kind.of_tau s
- | Cfield(f, _) -> sort_of_object (Ctypes.object_of f.ftype)
+ | Cfield(f, KValue) -> sort_of_object (Ctypes.object_of f.ftype)
+ | Cfield(f, KInit) -> init_sort_of_object (Ctypes.object_of f.ftype)
end
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 2ea0276c9b7..e82c635975b 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1338,6 +1338,8 @@ struct
let p = Vset.in_range (e_var k) a b in
let ofs = ofs_shift elt (e_var k) ofs in
let obj_x = Ctypes.object_of x.vtype in
+ let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj_x)) in
+ (memvar_set_init seq (Val(m,x,[])) init) ::
Assert(monotonic_initialized seq obj_x x []) ::
(assigned_genset seq [k] m x ofs p)
@@ -1350,6 +1352,8 @@ struct
M.assigned (mseq_of_seq seq) obj (Sdescr(xs,mloc_of_path m x ofs,p))
| Val((CVAL|CREF) as m,x,ofs) ->
let obj_x = Ctypes.object_of x.vtype in
+ let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj_x)) in
+ (memvar_set_init seq (Val(m,x,[])) init) ::
Assert(monotonic_initialized seq obj_x x []) ::
(assigned_genset seq xs m x ofs p)
--
GitLab