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