Predicate cmpWithLinearBound
Holds if guard
is a comparison operation (<
, <=
, >
, >=
,
==
or !=
), one of its arguments is equivalent (up to
associativity, commutativity and distributivity or the simple
arithmetic operations) to p*v + q
(for some p
and q
),
direction
describes whether guard
give an upper or lower bound
on v
, and branch
indicates which control-flow branch this
bound is valid on.
For example, if guard
is 2*v + 3 > 10
then
cmpWithLinearBound(guard, v, Greater(), true)
and
cmpWithLinearBound(guard, v, Lesser(), false)
hold.
If guard
is 4 - v > 5
then
cmpWithLinearBound(guard, v, Lesser(), true)
and
cmpWithLinearBound(guard, v, Greater(), false)
hold.
If an actual bound for v
is needed, use upperBound
or lowerBound
.
This predicate can be used if you just want to check whether a variable
is bounded, or to restrict a more expensive analysis to just guards that
bound a variable.
Import path
import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
predicate cmpWithLinearBound(ComparisonOperation guard, VariableAccess v, RelationDirection direction, boolean branch)