Provides a library for reasoning about control flow at the granularity of individual nodes in the control-flow graph.
Provides a library for reasoning about control flow at the granularity of basic blocks. This is usually much more efficient than reasoning directly at the level of
Provides predicates that should be exported as if they were top-level predicates in
Provides classes and predicates for working with C/C++ code.
Holds if there is a control-flow edge from
An abstract class that can be extended to add additional edges to the control-flow graph. Instances of this class correspond to the source nodes of such edges, and the predicate
A control-flow node is either a statement or an expression; in addition, functions are control-flow nodes representing the exit point of the function. The graph represents one possible evaluation order out of all the ones the compiler might have picked.
An element that is convertible to