Holds if this split is left when control passes from pred to succ with
completion c.
Invariant: hasExit(pred, succ, c) implies succ(pred, succ, c).
predicate hasExit(ControlFlowElement pred, ControlFlowElement succ, Completion c)Holds if this split is left when control passes from pred to succ with
completion c.
Invariant: hasExit(pred, succ, c) implies succ(pred, succ, c).
predicate hasExit(ControlFlowElement pred, ControlFlowElement succ, Completion c)