module Make:functor (
C
:
Wp.Sigs.Chunk
) ->
functor (
H
:
Qed.Collection.S
with type t = C.t
) ->
Wp.Sigs.Sigma
with type chunk = C.t and module Chunk = H
Parameters: |
|
type
chunk
The type of memory chunks.
module Chunk:Qed.Collection.S
with type t = chunk
typedomain =
Chunk.Set.t
Memory footprint.
type
t
Environment assigning logic variables to chunk.
Memory chunk variables are assigned lazily. Hence, the vector is empty unless a chunk is accessed. Pay attention to this when you merge or havoc chunks.
New chunks are generated from the context pool of Lang.freshvar
.
val pretty : Stdlib.Format.formatter -> t -> unit
For debugging purpose
val create : unit -> t
Initially empty environment.
val mem : t -> chunk -> bool
Whether a chunk has been assigned.
val get : t -> chunk -> Wp.Lang.F.var
Lazily get the variable for a chunk.
val value : t -> chunk -> Wp.Lang.F.term
Same as Lang.F.e_var
of get
.
val copy : t -> t
Duplicate the environment. Fresh chunks in the copy are not duplicated into the source environment.
val join : t -> t -> Wp.Passive.t
Make two environment pairwise equal via the passive form.
Missing chunks in one environment are added with the corresponding variable of the other environment. When both environments don't agree on a chunk, their variables are added to the passive form.
val assigned : pre:t ->
post:t -> domain -> Wp.Lang.F.pred Bag.t
Make chunks equal outside of some domain.
This is similar to join
, but outside the given footprint of an
assigns clause. Although, the function returns the equality
predicates instead of a passive form.
Like in join
, missing chunks are reported from one side to the
other one, and common chunks are added to the equality bag.
val choose : t -> t -> t
Make the union of each sigma, choosing the minimal variable in case of conflict. Both initial environments are kept unchanged.
val merge : t ->
t -> t * Wp.Passive.t * Wp.Passive.t
Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. Both initial environments are kept unchanged.
val merge_list : t list -> t * Wp.Passive.t list
Same than Wp.Sigs.Sigma.merge
but for a list of sigmas. Much more efficient
than folding merge step by step.
val iter : (chunk -> Wp.Lang.F.var -> unit) -> t -> unit
Iterates over the chunks and associated variables already accessed so far in the environment.
val iter2 : (chunk -> Wp.Lang.F.var option -> Wp.Lang.F.var option -> unit) ->
t -> t -> unit
Same as iter
for both environments.
val havoc_chunk : t -> chunk -> t
Generate a new fresh variable for the given chunk.
val havoc : t -> domain -> t
All the chunks in the provided footprint are generated and made fresh.
Existing chunk variables outside the footprint are copied into the new
environment. The original environement itself is kept unchanged. More
efficient than iterating havoc_chunk
over the footprint.
val havoc_any : call:bool -> t -> t
All the chunks are made fresh. As an optimisation,
when ~call:true
is set, only non-local chunks are made fresh.
Local chunks are those for which Chunk.is_frame
returns true
.
val remove_chunks : t -> domain -> t
Return a copy of the environment where chunks in the footprint have been removed. Keep the original environment unchanged.
val domain : t -> domain
Footprint of a memory environment. That is, the set of accessed chunks so far in the environment.
val union : domain -> domain -> domain
Same as Chunk.Set.union
val empty : domain
Same as Chunk.Set.empty
val writes : t Wp.Sigs.sequence -> domain
writes s
indicates which chunks are new in s.post
compared
to s.pre
.