module type Sigma =sig
..end
Represents the content of the memory, via a vector of logic
variables for each memory chunk.
type
chunk
module Chunk:Qed.Collection.S
with type t = chunk
typedomain =
Chunk.Set.t
type
t
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 : Format.formatter -> t -> unit
val create : unit -> t
val mem : t -> chunk -> bool
val get : t -> chunk -> Wp.Lang.F.var
val value : t -> chunk -> Wp.Lang.F.term
Lang.F.e_var
of get
.val copy : t -> t
val join : t -> t -> Wp.Passive.t
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
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
val merge : t ->
t -> t * Wp.Passive.t * Wp.Passive.t
val merge_list : t list -> t * Wp.Passive.t list
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
val iter2 : (chunk -> Wp.Lang.F.var option -> Wp.Lang.F.var option -> unit) ->
t -> t -> unit
iter
for both environments.val havoc_chunk : t -> chunk -> t
val havoc : t -> domain -> t
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
~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
val domain : t -> domain
val union : domain -> domain -> domain
Chunk.Set.union
val empty : domain
Chunk.Set.empty
val writes : t Wp.Sigs.sequence -> domain
writes s
indicates which chunks are new in s.post
compared
to s.pre
.