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.RangeAnalysisUtilspredicate cmpWithLinearBound(ComparisonOperation guard, VariableAccess v, RelationDirection direction, boolean branch)