diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 5c8b21c9784d4b7ad35602673189459350cb5cae..d26aee33e7d63313fd60a43d4d65ceaa2d7354db 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -133,6 +133,9 @@ and init_comp_value value ci =
 let initialized_obj = init_value e_true
 let uninitialized_obj = init_value e_false
 
+let always_initialized x =
+  (x.vformal || x.vglob) && not @@ Cil.isStructOrUnionType x.vtype
+
 (* -------------------------------------------------------------------------- *)
 (* --- Length of empty compinfos                                          --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 01fd0ed8bdff0d9922e7dca7b4f84b41701d5838..c9d70fa788fe5b589937095d80429bcb20a74083 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -99,6 +99,7 @@ val logic_constant : logic_constant -> term
 val constant_exp : exp -> term
 val constant_term : Cil_types.term -> term
 
+val always_initialized: varinfo -> bool
 val initialized_obj: c_object -> term
 val uninitialized_obj: c_object -> term
 
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 802617a661a7ef5a6cd7ecfe6d8c57a5cb29aaf7..abf67a6cb7c4af3ce67261a735ecfe22503268ff 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -579,8 +579,7 @@ module BASE = WpContext.Generator(Varinfo)
 
       let initialization prefix x base =
         match sizeof x with
-        | Some size
-          when (x.vformal || x.vglob) && not(Cil.isStructOrUnionType x.vtype) ->
+        | Some size when Cvalues.always_initialized x ->
             let a = Lang.freshvar ~basename:"init" t_init in
             let m = e_var a in
             let init_access =
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index c2897b53872b712cefd9917d1ceb31128a0c35b6..f52667de01c571a2691cd026d23888b0e89aec09 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -738,9 +738,6 @@ struct
   (* ---  Memory Load                                                       --- *)
   (* -------------------------------------------------------------------------- *)
 
-  let always_init vi =
-    (vi.vglob || vi.vformal) && not @@ Cil.isStructOrUnionType vi.vtype
-
   let rec access_gen kind a = function
     | [] -> a
     | Field f :: ofs -> access_gen kind (e_getfield a (Cfield (f, kind))) ofs
@@ -786,7 +783,7 @@ struct
   let load_init sigma obj = function
     | Ref _ ->
         e_true
-    | Val((CREF|CVAL),x,_) when always_init x ->
+    | Val((CREF|CVAL),x,_) when Cvalues.always_initialized x ->
         Cvalues.initialized_obj obj
     | Val((CREF|CVAL),x,ofs) ->
         access_init (get_init_term sigma x) ofs
@@ -1148,7 +1145,7 @@ struct
           | Val(m,x,p) ->
               if is_heap_allocated m then
                 M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
-              else if always_init x then
+              else if Cvalues.always_initialized x then
                 try valid_offset RW (vobject m x) p
                 with ShiftMismatch -> shift_mismatch l
               else
@@ -1174,7 +1171,7 @@ struct
                   let p, a, b = normalize elt p in
                   let in_array = valid_range RW (vobject m x) p (elt, a, b) in
                   let initialized =
-                    if always_init x then p_true
+                    if Cvalues.always_initialized x then p_true
                     else initialized_range sigma (vobject m x) x p a b
                   in
                   F.p_imply (F.p_leq a b) (p_and in_array initialized)
@@ -1263,7 +1260,8 @@ struct
     | Leave -> []
     | Enter ->
         let init_status v =
-          if v.vdefined || always_init v || not @@ is_mvar_alloc v then None
+          if v.vdefined || Cvalues.always_initialized v || not@@ is_mvar_alloc v
+          then None
           else
             let i = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in
             Some (Lang.F.p_equal (access_init (get_init_term seq.post v) []) i)
@@ -1377,7 +1375,7 @@ struct
   (* -------------------------------------------------------------------------- *)
 
   let rec monotonic_initialized seq obj x ofs =
-    if always_init x then p_true
+    if Cvalues.always_initialized x then p_true
     else
       match obj with
       (* Structure initialization is not monotonic *)
@@ -1611,7 +1609,9 @@ struct
   let domain obj l =
     match l with
     | Ref x | Val((CVAL|CREF),x,_) ->
-        let init = if not @@ always_init x then [ Init x ] else [] in
+        let init =
+          if not @@ Cvalues.always_initialized x then [ Init x ] else []
+        in
         Heap.Set.of_list ((Var x) :: init)
     | Loc _ | Val((CTXT _|CARR _|HEAP),_,_) ->
         M.Heap.Set.fold