module Sigma: sig
.. end
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 -> chunk -> Lang.F.var
val mem : MemVar.Make.sigma -> chunk -> bool
val value : MemVar.Make.sigma -> chunk -> Lang.F.term
val iter : (chunk -> Lang.F.var -> unit) -> MemVar.Make.sigma -> unit
val iter2 : (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 -> 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