module Sigma: Wp.Memory.Sigma
with type chunk = Chunk.t
and type domain = Heap.set
type
chunk
type
domain
type
t
val create : unit -> t
val copy : t -> t
val merge : t ->
t -> t * Wp.Passive.t * Wp.Passive.t
val join : t -> t -> Wp.Passive.t
pairwise equal
val assigned : t ->
t -> domain -> Wp.Lang.F.pred Bag.t
equal chunks outside domain
val mem : t -> chunk -> bool
val get : t -> chunk -> Wp.Lang.F.var
val value : t -> chunk -> Wp.Lang.F.term
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
val havoc : t -> domain -> t
val havoc_chunk : t -> chunk -> t
val havoc_any : call:bool -> t -> t
val domain : t -> domain
val union : domain -> domain -> domain
val empty : domain
val pretty : Format.formatter -> t -> unit