Predicate SuccSplits::case2aFromRank
Case 2a.
As opposed to the other cases, in this case we need to construct a new set
of splits succSplits. Since this involves constructing the very IPA type,
we cannot recurse directly over the structure of succSplits. Instead, we
recurse over the ranks of all splits that might be in succSplits.
- Invariant 1 holds in the base case,
- invariant 2 holds for all splits with rank at least
rnk, - invariant 3 holds for all splits in
predSplits, - invariant 4 holds for all splits in
succSplitswith rank at leastrnk, and - invariant 4 holds for all splits in
succSplitswith rank at leastrnk.
Import path
import codeql.ruby.controlflow.internal.ControlFlowGraphImplSharedpredicate case2aFromRank(ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits, Completion c, int rnk)