Skip to content

Commit 10585e7

Browse files
committed
C++: Support widening casts in range analysis
This makes sure we can conclude from `(int)myShort == 0` that `myShort` is 0 even though we can no longer conclude from `(short)myInt == 0` that `myInt` is 0. Without this, we lost a good result in the test for `InfiniteLoopWithUnsatisfiableExitCondition.ql`.
1 parent 640f900 commit 10585e7

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,18 @@ predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q) {
204204
| linearAccess(unaryPlusExpr.getOperand().getFullyConverted(), v, p, q) and
205205
expr = unaryPlusExpr)
206206
or
207+
// (larger_type)(p*v+q) == p*v + q
208+
exists (Cast cast
209+
| linearAccess(cast.getExpr(), v, p, q) and
210+
typeLowerBound(cast.getType()) <= typeLowerBound(cast.getExpr().getType()) and
211+
typeUpperBound(cast.getType()) >= typeUpperBound(cast.getExpr().getType()) and
212+
expr = cast)
213+
or
214+
// (p*v+q) == p*v + q
215+
exists (ParenthesisExpr paren
216+
| linearAccess(paren.getExpr(), v, p, q) and
217+
expr = paren)
218+
or
207219
// -(a*v+b) == -a*v + (-b)
208220
exists (UnaryMinusExpr unaryMinusExpr, float a, float b
209221
| linearAccess(unaryMinusExpr.getOperand().getFullyConverted(), v, a, b) and

0 commit comments

Comments
 (0)