module SIGMA: Sigma.Make
(
VAR
)
(
HEAP
)
type
chunk = C.t
type
domain = H.set
type
t = {
|
id : int ; |
|
mutable map : Lang.F.var H.map ; |
}
val create : unit -> t
val copy : t -> t
val merge : t -> t -> t * Passive.t * Passive.t
val get : t -> H.Map.key -> Lang.F.var
val mem : t -> H.Map.key -> bool
val join : t -> t -> Passive.t
val assigned : t -> t -> H.Set.t -> Lang.F.pred Bag.t
val value : t -> H.Map.key -> Lang.F.term
val iter : (H.Map.key -> Lang.F.var -> unit) -> t -> unit
val iter2 : (H.Map.key -> Lang.F.var option -> Lang.F.var option -> unit) ->
t -> t -> unit
val havoc : t -> H.Set.t -> t
val havoc_chunk : t -> H.Map.key -> t
val havoc_any : call:bool -> t -> t
val domain : t -> H.Map.domain
val pretty : Format.formatter -> t -> unit