[wp] MemVar initialized fixes issue with typing + havoc some variables

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
 

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)