Module Hcexprs.HCEToZone

module HCEToZone: sig .. end

Maps from symbolic expressions to their memory dependencies, expressed as a Locations.Zone.t.


include Datatype.S_with_collections
val empty : t
val add : Hcexprs.HCE.t -> Locations.Zone.t -> t -> t
val remove : Hcexprs.HCE.t -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val is_included : t -> t -> bool
val find : Hcexprs.HCE.t -> t -> Locations.Zone.t
val find_default : Hcexprs.HCE.t -> t -> Locations.Zone.t

returns the empty set when the key is not bound