Provides a library for working with local (intra-procedural) control-flow reachability involving stack variables.
Provides classes and predicates for working with C/C++ code.
Loop invariant for
A reachability analysis for control-flow nodes involving stack variables. This defines sources, sinks, and any other configurable aspect of the analysis. Multiple analyses can coexist. To create an analysis, extend this class with a subclass whose characteristic predicate is a unique singleton string. For example, write
Reachability analysis for control-flow nodes involving stack variables. Unlike