C++: Convert 'getBranchSuccessor' to use abstract values.

This commit is contained in:
Mathias Vorreiter Pedersen
2024-03-15 16:51:15 +00:00
parent b7292fbc67
commit f4eb5f5a2d

View File

@@ -359,15 +359,21 @@ class IRGuardCondition extends Instruction {
* return x;
* ```
*/
private IRBlock getBranchSuccessor(boolean testIsTrue) {
private IRBlock getBranchSuccessor(AbstractValue v) {
branch.(ConditionalBranchInstruction).getCondition() = this and
(
testIsTrue = true and
exists(BooleanValue bv | bv = v |
bv.getValue() = true and
result.getFirstInstruction() = branch.(ConditionalBranchInstruction).getTrueSuccessor()
or
testIsTrue = false and
bv.getValue() = false and
result.getFirstInstruction() = branch.(ConditionalBranchInstruction).getFalseSuccessor()
)
or
exists(SwitchInstruction switch, CaseEdge kind | switch = branch |
switch.getExpression() = this and
result.getFirstInstruction() = switch.getSuccessor(kind) and
kind = v.(MatchValue).getCase()
)
}
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */