Skip to content

Commit

Permalink
C++: Don't allow 'x < 0' as a barrier guard.
Browse files Browse the repository at this point in the history
  • Loading branch information
MathiasVP committed Oct 9, 2024
1 parent c883aa0 commit 61a012f
Showing 1 changed file with 4 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,11 @@ predicate isFlowSource(FS::FlowSource source, string sourceType) {

predicate guardChecks(IRGuardCondition g, Expr e, boolean branch) {
exists(Operand op | op.getDef().getConvertedResultExpression() = e |
// op < k
g.comparesLt(op, _, true, any(BooleanValue bv | bv.getValue() = branch))
// `op < k` is true and `k > 0`
g.comparesLt(op, any(int k | k > 0), true, any(BooleanValue bv | bv.getValue() = branch))
or
// op < _ + k
g.comparesLt(op, _, _, true, branch)
// `op < _ + k` is true and `k > 0`.
g.comparesLt(op, _, any(int k | k > 0), true, branch)
or
// op == k
g.comparesEq(op, _, true, any(BooleanValue bv | bv.getValue() = branch))
Expand Down

0 comments on commit 61a012f

Please sign in to comment.