From 03bf686f1cdf70f18ca7c98530593249af09391d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 7 Apr 2020 17:28:47 +0200
Subject: [PATCH] [wp] MemLoader generates initialized for segments
---
src/plugins/wp/MemLoader.ml | 13 +++++++++++++
src/plugins/wp/MemLoader.mli | 2 +-
src/plugins/wp/MemRegion.ml | 3 +--
src/plugins/wp/MemTyped.ml | 14 +-------------
4 files changed, 16 insertions(+), 16 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index e9e806770dc..ac6e5cbcda1 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 747ebaf8d7a..7240bbcc920 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 233936e0491..ec013da03bc 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 7aa36305771..51d49141a7e 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
--
GitLab