Module AccessTree.PathSet

Concise representation of a set of access paths

Parameters

Signature

include module type of sig ... end
module TraceDomain : sig ... end
module AccessMap : sig ... end
module BaseMap = AccessPath.BaseMap
type node = TraceDomain.t * tree
and tree = Make(Absint.AbstractDomain.BooleanOr)(Config).tree =
| Subtree of node AccessMap.t

map from access -> nodes. a leaf is encoded as an empty map

| Star

special leaf for starred access paths

type t = node BaseMap.t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool
val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val bottom : t
val is_bottom : t -> bool
val empty_node : node
val make_node : TraceDomain.t -> node AccessMap.t -> node
val make_access_node : TraceDomain.t -> AccessPath.access -> TraceDomain.t -> node

for testing only

val make_normal_leaf : TraceDomain.t -> node

create a leaf node with no successors

val make_starred_leaf : TraceDomain.t -> node

create a leaf node with a wildcard successor

val get_node : AccessPath.Abs.t -> t -> node option

retrieve the node associated with the given access path

val get_trace : AccessPath.Abs.t -> t -> TraceDomain.t option

retrieve the trace associated with the given access path

val add_node : AccessPath.Abs.t -> node -> t -> t

add the given access path to the tree and associate its last access with the given node. if any of the accesses in the path are not already present in the tree, they will be added with empty traces associated with each of the inner nodes.

val add_trace : AccessPath.Abs.t -> TraceDomain.t -> t -> t

add the given access path to the tree and associate its last access with the given trace. if any of the accesses in the path are not already present in the tree, they will be added with empty traces associated with each of the inner nodes.

val node_join : node -> node -> node

join two nodes

val fold : ('a -> AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a

apply a function to each (access path, node) pair in the tree.

val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.t -> 'a) -> t -> 'a -> 'a
val exists : (AccessPath.Abs.t -> node -> bool) -> t -> bool
val iter : (AccessPath.Abs.t -> node -> unit) -> t -> unit
val depth : t -> int

number of traces in the tallest branch of the tree

val pp_node : Stdlib.Format.formatter -> node -> unit
val mem : AccessPath.Abs.t -> t -> bool