Module type Absint__AccessTree.S
tree of (trace, access path) associations organized by structure of access paths
module AccessMap : IStdlib.PrettyPrintable.PPMap with type PPMap.key = Absint.AccessPath.access
module BaseMap = Absint.AccessPath.BaseMap
type node
= TraceDomain.t * tree
and 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
map from base var -> access subtree. Here's how to represent a few different kinds of trace * access path associations:
(x, T) := { x |-> (T, Subtree {}) }
(x.f, T) := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) }
(x*, T) := { x |-> (T, Star) }
(x.f*, T) := { x |-> (empty, Subtree { f |-> (T, Star) }) }
(x, T1), (y, T2) := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) }
(x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}),
g |-> (T2, Subtree {}) }) }
include Absint.AbstractDomain.WithBottom with type t = node BaseMap.t
include Absint.AbstractDomain.S
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val bottom : t
The bottom value of the domain.
val is_bottom : t -> bool
Return true if this is the bottom value
val empty_node : node
val make_node : TraceDomain.t -> node AccessMap.t -> node
val make_access_node : TraceDomain.t -> Absint.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 : Absint.AccessPath.Abs.t -> t -> node option
retrieve the node associated with the given access path
val get_trace : Absint.AccessPath.Abs.t -> t -> TraceDomain.t option
retrieve the trace associated with the given access path
val add_node : Absint.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 : Absint.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 fold : ('a -> Absint.AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a
apply a function to each (access path, node) pair in the tree.
val trace_fold : ('a -> Absint.AccessPath.Abs.t -> TraceDomain.t -> 'a) -> t -> 'a -> 'a
val exists : (Absint.AccessPath.Abs.t -> node -> bool) -> t -> bool
val iter : (Absint.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