diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index e9e806770dcd35fc4238f62e8b9addc31b0d3db7..ac6e5cbcda1d19012b80a37f5a0ea87ae09c44ca 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -433,6 +433,19 @@ struct
   let initialized_loc sigma obj loc =
     initialized_term obj (initvalue sigma obj loc)
 
+  let initialized sigma = function
+    | Rloc(obj, loc) -> initialized_loc sigma obj loc
+    | Rrange(loc, obj, Some low, Some up) ->
+        let x = Lang.freshvar ~basename:"i" Lang.t_int in
+        let v = e_var x in
+        let hyps = [ p_leq low v ; p_leq v up] in
+        let loc = M.shift loc obj v in
+        p_forall [x] (p_hyps hyps (initialized_loc sigma obj loc))
+    | Rrange(_l, _, low, up) ->
+        Wp_parameters.abort ~current:true
+          "Invalid infinite range @[<hov 2>+@,(%a@,..%a)@]"
+          Vset.pp_bound low Vset.pp_bound up
+
   (* -------------------------------------------------------------------------- *)
   (* --- Stored & Copied                                                    --- *)
   (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 747ebaf8d7a108b96a1c6673ea478f1086920ddd..7240bbcc920442864f2268a454177550a482b6e4 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -97,7 +97,7 @@ sig
 
   val assigned : M.Sigma.t sequence -> c_object -> M.loc sloc -> equation list
 
-  val initialized_loc : M.Sigma.t -> c_object -> M.loc -> pred
+  val initialized : M.Sigma.t -> M.loc rloc -> pred
 
 end
 
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 233936e0491d31cd56dbf7c79961db2915b09b15..ec013da03bcc008997900d389705f7c2c4e29494 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -826,7 +826,7 @@ let loadvalue = LOADER.loadvalue
 let stored = LOADER.stored
 let copied = LOADER.copied
 let assigned = LOADER.assigned
-let initialized_loc = LOADER.initialized_loc
+let initialized = LOADER.initialized
 
 let domain = LOADER.domain
 
@@ -891,6 +891,5 @@ let frame _sigma = []
 let alloc sigma _xs = sigma
 let scope _seq _s _xs = []
 let valid _sigma _acs _l = error "Validity not yet implemented"
-let initialized _sigma _l = error "Initialization not yet implemented"
 let invalid _sigma _l = error "Validity not yet implemented"
 let global _sigma _p = F.p_true
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 7aa363057718e90d9f503024c7dcd2182f20d666..51d49141a7ed7131f5eb22ae3fc461a33ffac94c 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -995,7 +995,7 @@ let load = LOADER.load
 let stored = LOADER.stored
 let copied = LOADER.copied
 let assigned = LOADER.assigned
-let initialized_loc = LOADER.initialized_loc
+let initialized = LOADER.initialized
 let domain = LOADER.domain
 
 (* -------------------------------------------------------------------------- *)
@@ -1047,18 +1047,6 @@ let segment phi = function
 let valid sigma acs = segment (s_valid sigma acs)
 let invalid sigma = segment (s_invalid sigma)
 
-let initialized sigma = function
-  | Rloc(obj, loc) -> initialized_loc sigma obj loc
-  | Rrange(loc, obj, Some low, Some up) ->
-      let v = e_var (Lang.freshvar ~basename:"i" Lang.t_int) in
-      let hyps = [ p_leq low v ; p_leq v up] in
-      let loc = shift loc obj v in
-      p_hyps hyps (initialized_loc sigma obj loc)
-  | Rrange(l, _, low, up) ->
-      Wp_parameters.abort ~current:true
-        "Invalid infinite range @[<hov 2>%a+@,(%a@,..%a)@]"
-        F.pp_term l Vset.pp_bound low Vset.pp_bound up
-
 let frame sigma =
   let wellformed_frame phi chunk =
     if Sigma.mem sigma chunk