Module StateTracking

Provides classes and predicates for tracking global state across the control flow and call graphs.

NOTE: State tracking tracks both whether a state may apply to a given node in a given context and whether it may not apply. That state.appliesTo(f, ctx) holds implies nothing about whether state.mayNotApplyTo(f, ctx) holds. Neither may hold which merely means that f with context ctx is not reached during the analysis. Conversely, both may hold, which means that state may or may not apply depending on how f was reached.