sig
type t = MemVar.Make.sigma
type chunk = MemVar.Make.Chunk.t
type domain = MemVar.Make.Heap.set
val create : unit -> MemVar.Make.sigma
val copy : MemVar.Make.sigma -> MemVar.Make.sigma
val merge :
MemVar.Make.sigma ->
MemVar.Make.sigma -> MemVar.Make.sigma * Passive.t * Passive.t
val join : MemVar.Make.sigma -> MemVar.Make.sigma -> Passive.t
val get : MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> Lang.F.var
val mem : MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> bool
val value : MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> Lang.F.term
val iter :
(MemVar.Make.Sigma.chunk -> Lang.F.var -> unit) ->
MemVar.Make.sigma -> unit
val iter2 :
(MemVar.Make.Sigma.chunk ->
Lang.F.var option -> Lang.F.var option -> unit) ->
MemVar.Make.sigma -> MemVar.Make.sigma -> unit
val domain_partition :
MemVar.Make.Heap.Set.t ->
MemVar.Make.HEAP.Set.t * MemVar.Make.TALLOC.Set.t * M.Heap.Set.t
val domain_var : MemVar.Make.HEAP.Set.t -> MemVar.Make.Heap.Set.t
val domain_alloc : MemVar.Make.TALLOC.Set.t -> MemVar.Make.Heap.Set.t
val domain_mem : M.Heap.Set.t -> MemVar.Make.Heap.Set.t
val assigned :
MemVar.Make.sigma ->
MemVar.Make.sigma -> MemVar.Make.Heap.Set.t -> Lang.F.pred Bag.t
val havoc :
MemVar.Make.sigma -> MemVar.Make.Heap.Set.t -> MemVar.Make.sigma
val havoc_chunk :
MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> MemVar.Make.sigma
val havoc_any : call:bool -> MemVar.Make.sigma -> MemVar.Make.sigma
val domain : MemVar.Make.sigma -> MemVar.Make.Heap.Set.t
val pretty : Format.formatter -> MemVar.Make.sigma -> unit
end