[wp] MemLoader generates initialized for segments

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                                                    --- *)
   (* -------------------------------------------------------------------------- *)

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
 

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

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