sig
type chunk
type domain
type t
val create : unit -> Wp.Memory.Sigma.t
val copy : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t
val merge :
Wp.Memory.Sigma.t ->
Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t * Wp.Passive.t * Wp.Passive.t
val join : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> Wp.Passive.t
val assigned :
Wp.Memory.Sigma.t ->
Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Lang.F.pred Bag.t
val mem : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> bool
val get : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.var
val value : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.term
val iter :
(Wp.Memory.Sigma.chunk -> Wp.Lang.F.var -> unit) ->
Wp.Memory.Sigma.t -> unit
val iter2 :
(Wp.Memory.Sigma.chunk ->
Wp.Lang.F.var option -> Wp.Lang.F.var option -> unit) ->
Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> unit
val havoc :
Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.t
val havoc_chunk :
Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Memory.Sigma.t
val havoc_any : call:bool -> Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t
val domain : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain
val union :
Wp.Memory.Sigma.domain ->
Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.domain
val empty : Wp.Memory.Sigma.domain
val pretty : Format.formatter -> Wp.Memory.Sigma.t -> unit
end