Module MakeImplStage1::ImplStage1::Stage1

Holds if flow may enter through p and reach a return node making p a candidate for the origin of a summary.

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

Holds if c is the target of both a read and a store in the flow covered by revFlow.