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(), false)
and
cmpWithLinearBound(guard, v, Greater(), true)
hold.
A more sophisticated predicate, such as boundFromGuard
, is needed
to compute an actual bound for v
. 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
)