Module MakeImpl::Impl::MkStage::Stage

Holds if node is reachable with access path ap from a source.

Holds if ap is recorded as the summary context for flow reaching node and remains relevant for the following pruning stage.

Holds if node with access path ap is part of a path from a source to a sink.

Provides a graph representation of the data flow in this stage suitable for use in a path-problem query.

Provides a big-step relation for local flow steps.

Holds if node1 can step to node2 in one or more local steps.