module Sigma:Sigs.Sigma
with type chunk = Chunk.t and module Chunk = Heap
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 -> Lang.F.var
val value : t -> chunk -> Lang.F.term
Lang.F.e_var
of get
.val copy : t -> t
val join : t -> t -> 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 -> 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 * Passive.t * Passive.t
val merge_list : t list -> t * Passive.t list
Sigs.Sigma.merge
but for a list of sigmas. Much more efficient
than folding merge step by step.val iter : (chunk -> Lang.F.var -> unit) -> t -> unit
val iter2 : (chunk -> Lang.F.var option -> 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 Sigs.sequence -> domain
writes s
indicates which chunks are new in s.post
compared
to s.pre
.