C++: More fixes to overflow detection

This commit is contained in:
Robert Marsh
2023-04-04 09:31:03 -04:00
parent 2606abfc64
commit e4ae957cdd
4 changed files with 139 additions and 107 deletions

View File

@@ -941,6 +941,17 @@ module RangeStage<
semExprDoesntOverflow(upper.booleanNot(), e)
or
not potentiallyOverflowingExpr(upper.booleanNot(), e)
or
initialBounded(e, any(SemZeroBound z), _, upper.booleanNot(), _, _, _)
or
exists(D::Delta otherDelta |
initialBounded(e, _, otherDelta, upper.booleanNot(), _, _, _) and
(
upper = true and D::toFloat(otherDelta) >= 0
or
upper = false and D::toFloat(otherDelta) <= 0
)
)
)
}
@@ -952,16 +963,14 @@ module RangeStage<
(
positively = true and
(
not semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TPos()
or
not semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TPos()
semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TPos() and
semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TPos()
)
or
positively = false and
(
not semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TNeg()
or
not semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TNeg()
semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TNeg() and
semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TNeg()
)
)
or
@@ -972,16 +981,14 @@ module RangeStage<
(
positively = true and
(
not semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TPos()
or
not semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TNeg()
semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TPos() and
semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TNeg()
)
or
positively = false and
(
not semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TNeg()
or
not semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TPos()
semExprSign(expr.(SemBinaryExpr).getLeftOperand()) = TNeg() and
semExprSign(expr.(SemBinaryExpr).getRightOperand()) = TPos()
)
)
or

View File

@@ -0,0 +1,25 @@
import cpp
import experimental.semmle.code.cpp.semantic.analysis.SimpleRangeAnalysis
import TestUtilities.InlineExpectationsTest
class RangeAnalysisTest extends InlineExpectationsTest {
RangeAnalysisTest() { this = "RangeAnalysisTest" }
override string getARelevantTag() { result = "overflow" }
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(Expr e |
/*call.getArgument(0) = e and
call.getTarget().hasName("range") and*/
tag = "overflow" and
element = e.toString() and
location = e.getLocation() and
value =
strictconcat(string s |
s = "+" and exprMightOverflowPositively(e)
or
s = "-" and exprMightOverflowNegatively(e)
)
)
}
}

View File

@@ -8,7 +8,7 @@ int test1(struct List* p) {
int count = 0;
for (; p; p = p->next) {
count = count+1;
range(count);
range(count); // $ range===count:p+1
}
range(count);
return count;
@@ -39,14 +39,14 @@ int test4() {
int i = 0;
int total = 0;
for (i = 0; i < 2; i = i+1) {
range(i); // $ range=<=1 MISSING: range=>=0
range(i); // $ range=<=1 range=>=0
range(total);
total += i;
range(total); // $ range=<=i+1 range=<=i+1 range=>=0 range=>=i+0
range(total); // $ range=<=i+1 range=<=i+1 MISSING: range=>=0 range=>=i+0
}
range(total); // $ range=>=0
range(total); // $ MISSING: range=>=0
range(i); // $ range===2
range(total + i); // $ range===i+2 range=>=2 range=>=i+0
range(total + i); // $ range=<=i+2 MISSING: range===i+2 range=>=2 range=>=i+0
return total + i;
}
@@ -55,13 +55,13 @@ int test5() {
int total = 0;
for (i = 0; i < 2; i++) {
range(i); // $ range=<=1 range=>=0
range(total); // $ range=>=0
range(total); // $ MISSING: range=>=0
total += i;
range(total); // $ range=<=i+1 range=>=0 range=>=i+0
range(total); // $ range=<=i+1 MISSING: range=>=0 range=>=i+0
}
range(total); // $ range=>=0
range(total); // $ MISSING: range=>=0
range(i); // $ range===2
range(total + i); // $ range===i+2 range=>=2 range=>=i+0
range(total + i); // $ range=<=i+2 MISSING: range===i+2 range=>=2 range=>=i+0
return total + i;
}
@@ -70,9 +70,9 @@ int test6() {
int total = 0;
for (i = 0; i+2 < 4; i = i+1) {
range(i); // $ range=<=1 range=>=0
range(total); // $ range=>=0
range(total); // $ MISSING: range=>=0
total += i;
range(total); // $ range=<=i+1 range=>=0 range=>=i+0
range(total); // $ range=<=i+1 MISSING: range=>=0 range=>=i+0
}
return total + i;
}
@@ -145,7 +145,7 @@ int test11(char *p) {
range(*p);
if (c != '\0') {
*p++ = '\0';
range(p);
range(p); // $ range===p+1
range(*p);
}
if (c == ':') {
@@ -155,7 +155,7 @@ int test11(char *p) {
if (c != '\0') {
range(c);
*p++ = '\0';
range(p);
range(p); // $ range=<=p+2 range===c+1 range=>=p+1
}
if (c != ',') {
return 1;
@@ -168,7 +168,7 @@ typedef unsigned long long size_type;
size_type test12_helper() {
static size_type n = 0;
return n++;
return n++; // $ overflow=+
}
int test12() {
@@ -177,7 +177,7 @@ int test12() {
{
range(Start); // $ MISSING:range=>=0
const size_type Length = test12_helper();
Start += Length + 1;
Start += Length + 1; // $ overflow=+
range(Start); // $ MISSING:range=>=1 MISSING:range=>=Start+1 MISSING:range=">=call to test12_helper+1"
}
range(Start); // $ MISSING:range=>=0
@@ -190,13 +190,13 @@ int test13(char c, int i) {
unsigned char uc = c;
range(uc);
unsigned int x = 0;
unsigned int y = x-1;
range(y); // $ range=>=-1
int z = i+1;
range(z);
range(c + i + uc + x + y + z); // $ range=>=1 range=">=... - ...+0"
range((double)(c + i + uc + x + y + z)); // $ range=>=1 range=">=... - ...+0"
return (double)(c + i + uc + x + y + z);
unsigned int y = x-1; // $ overflow=-
range(y); // $ range===-1 overflow=-
int z = i+1; // $ overflow=+
range(z); // $ range===i+1
range(c + i + uc + x + y + z); // $ overflow=+- overflow=+ overflow=- MISSING: range=>=1
range((double)(c + i + uc + x + y + z)); // $ overflow=+ overflow=+- overflow=- MISSING: range=>=1
return (double)(c + i + uc + x + y + z); // $ overflow=+- overflow=+ overflow=-
}
// Regression test for ODASA-6013.
@@ -213,8 +213,8 @@ int test14(int x) {
range(c0);
unsigned short s0 = x;
range(s0);
range(x0 + x1 + x2 + x3 + c0 + s0);
return x0 + x1 + x2 + x3 + c0 + s0;
range(x0 + x1 + x2 + x3 + c0 + s0); // $ overflow=+ overflow=+-
return x0 + x1 + x2 + x3 + c0 + s0; // $ overflow=+ overflow=+-
}
long long test15(long long x) {
@@ -242,8 +242,8 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=11 range=>=0
int c = -a;
range(c);
range(b+c); // $ range=<=11 range="<=+ ...:a+0" MISSING:range=">=- ...+0"
range(c); // $ range=<=0 range=>=-11
range(b+c); // $ range=<=11 range=>=-11 MISSING:range=">=- ...+0"
total += b+c;
range(total); // $ range=<=0+11 range=<=19 range=>=0-11 range=>=-19
}
@@ -272,8 +272,8 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=0 range=>=-7
int c = -a;
range(c);
range(b+c); // $ range=">=+ ...:a+0" range=>=-7 MISSING:range="<=- ...+0"
range(c); // $ range=<=7 range=>=0
range(b+c); // $ range=>=-7 range=<=7 MISSING:range="<=- ...+0"
total += b+c;
range(total); // $ range="<=- ...+7" range="<=- ...+15" range="<=- ...+33" range=">=- ...-7" range=">=- ...-15" range=">=- ...-33" range=<=0+44 range=<=52 range=>=0-44 range=>=-52
}
@@ -315,9 +315,9 @@ int test_mult01(int a, int b) {
if (3 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=23 range=>=-13
int r = a*b; // -143 .. 253
int r = a*b; // $ overflow=+- -143 .. 253
range(r);
total += r;
total += r; // $ overflow=+
range(total); // $ MISSING: range=">=... * ...+0"
}
if (3 <= a && a <= 11 && -13 <= b && b <= 0) {
@@ -326,7 +326,7 @@ int test_mult01(int a, int b) {
int r = a*b; // -143 .. 0
range(r); // $ range=<=0 range=>=-143
total += r;
range(total); // $ range=<=3+0 range=>=3-143
range(total); // $ range=>=3-143
}
if (3 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=3
@@ -334,9 +334,9 @@ int test_mult01(int a, int b) {
int r = a*b; // -143 .. -21
range(r); // $ range=<=-21 range=>=-143
total += r;
range(total); // $ range=<=3-21 range=>=3-143 range=>=3-286
range(total); // $ range=>=3-143 range=>=3-286
}
range(total); // $ range=<=3+0 range=>=3-143 range=>=3-286
range(total); // $ range=>=3-143 range=>=3-286
return total;
}
@@ -363,9 +363,9 @@ int test_mult02(int a, int b) {
if (0 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=0
range(b); // $ range=<=23 range=>=-13
int r = a*b; // -143 .. 253
int r = a*b; // $ overflow=+- -143 .. 253
range(r);
total += r;
total += r; // $ overflow=+
range(total); // $ MISSING: range=">=... * ...+0"
}
if (0 <= a && a <= 11 && -13 <= b && b <= 0) {
@@ -374,7 +374,7 @@ int test_mult02(int a, int b) {
int r = a*b; // -143 .. 0
range(r); // $ range=<=0 range=>=-143
total += r;
range(total); // $ range=<=0+0 range=>=0-143
range(total); // $ range=>=0-143
}
if (0 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=0
@@ -382,9 +382,9 @@ int test_mult02(int a, int b) {
int r = a*b; // -143 .. 0
range(r); // $ range=<=0 range=>=-143
total += r;
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
range(total); // $ range=>=0-143 range=>=0-286
}
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
range(total); // $range=>=0-143 range=>=0-286
return total;
}
@@ -395,7 +395,7 @@ int test_mult03(int a, int b) {
if (-17 <= a && a <= 11 && 5 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=-17
range(b); // $ range=<=23 range=>=5
int r = a*b; // -391 .. 253
int r = a*b; // $ overflow=+- -391 .. 253
range(r);
total += r;
range(total);
@@ -403,33 +403,33 @@ int test_mult03(int a, int b) {
if (-17 <= a && a <= 11 && 0 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=-17
range(b); // $ range=<=23 range=>=0
int r = a*b; // -391 .. 253
int r = a*b; // $ overflow=+- -391 .. 253
range(r);
total += r;
total += r; // $ overflow=+-
range(total);
}
if (-17 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=-17
range(b); // $ range=<=23 range=>=-13
int r = a*b; // -391 .. 253
int r = a*b; //3 $ overflow=+- -391 .. 25
range(r);
total += r;
total += r; // $ overflow=+-
range(total);
}
if (-17 <= a && a <= 11 && -13 <= b && b <= 0) {
range(a); // $ range=<=11 range=>=-17
range(b); // $ range=<=0 range=>=-13
int r = a*b; // -143 .. 221
int r = a*b; // $ overflow=+- -143 .. 221
range(r);
total += r;
total += r; // $ overflow=+-
range(total);
}
if (-17 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=-17
range(b); // $ range=<=-7 range=>=-13
int r = a*b; // -143 .. 221
int r = a*b; // $ overflow=+- -143 .. 221
range(r);
total += r;
total += r; // $ overflow=+-
range(total);
}
range(total);
@@ -458,9 +458,9 @@ int test_mult04(int a, int b) {
if (-17 <= a && a <= 0 && -13 <= b && b <= 23) {
range(a); // $ range=<=0 range=>=-17
range(b); // $ range=<=23 range=>=-13
int r = a*b; // -391 .. 221
int r = a*b; // $ overflow=+- -391 .. 221
range(r);
total += r;
total += r; // $ overflow=-
range(total); // $ MISSING: range="<=... * ...+0"
}
if (-17 <= a && a <= 0 && -13 <= b && b <= 0) {
@@ -469,7 +469,7 @@ int test_mult04(int a, int b) {
int r = a*b; // 0 .. 221
range(r); // $ range=<=221 range=>=0
total += r;
range(total); // $ range="<=- ...+221" range=">=- ...+0"
range(total); // $ range="<=- ...+221"
}
if (-17 <= a && a <= 0 && -13 <= b && b <= -7) {
range(a); // $ range=<=0 range=>=-17
@@ -477,9 +477,9 @@ int test_mult04(int a, int b) {
int r = a*b; // 0 .. 221
range(r); // $ range=<=221 range=>=0
total += r;
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
range(total); // $ range="<=- ...+221" range="<=- ...+442"
}
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
range(total); // $ range="<=- ...+221" range="<=- ...+442"
return total;
}
@@ -506,9 +506,9 @@ int test_mult05(int a, int b) {
if (-17 <= a && a <= -2 && -13 <= b && b <= 23) {
range(a); // $ range=<=-2 range=>=-17
range(b); // $ range=<=23 range=>=-13
int r = a*b; // -391 .. 221
int r = a*b; // $ overflow=+- -391 .. 221
range(r);
total += r;
total += r; // $ overflow=-
range(total); // $ MISSING: range="<=... * ...+0"
}
if (-17 <= a && a <= -2 && -13 <= b && b <= 0) {
@@ -517,7 +517,7 @@ int test_mult05(int a, int b) {
int r = a*b; // 0 .. 221
range(r); // $ range=<=221 range=>=0
total += r;
range(total); // $ range="<=- ...+221" range=">=- ...+0"
range(total); // $ range="<=- ...+221"
}
if (-17 <= a && a <= -2 && -13 <= b && b <= -7) {
range(a); // $ range=<=-2 range=>=-17
@@ -525,9 +525,9 @@ int test_mult05(int a, int b) {
int r = a*b; // 14 .. 221
range(r); // $ range=<=221 range=>=14
total += r;
range(total); // $ range="<=- ...+221" range="<=- ...+442" range=">=- ...+14"
range(total); // $ range="<=- ...+221" range="<=- ...+442"
}
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
range(total); // $ range="<=- ...+221" range="<=- ...+442"
return total;
}
@@ -539,9 +539,9 @@ int test16(int x) {
}
while (i < 3) {
range(i); // $ range=<=2 MISSING:range=>=0
range(i); // $ range=<=2 range=>=0
i++;
range(i); // $ range=<=3 MISSING:range=>=1 range="==... = ...:i+1" SPURIOUS:range="==... = ...:i+1"
range(i); // $ range=<=3 range=>=1 range="==... = ...:i+1" SPURIOUS:range="==... = ...:i+1"
}
range(d);
d = i;
@@ -586,7 +586,7 @@ unsigned int test_ternary01(unsigned int x) {
(range(x), 500); // y4 <= 500
range(y4);
y5 = (x+1) ?:
(range(x), 500); // $ range===-1
(range(x), 500); // $ overflow=- range===-1
range(y5); // y5 <= 300
y6 = ((unsigned char)(x+1)) ?:
(range(x), 5); // $ range=<=299
@@ -598,8 +598,8 @@ unsigned int test_ternary01(unsigned int x) {
(range(x), 500); // $ range=<=299
range(y8); // y8 <= 300
}
range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8;
range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ overflow=+ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8; // $ overflow=+
}
// Test ternary expression lower bounds.
@@ -628,8 +628,8 @@ unsigned int test_ternary02(unsigned int x) {
(range(x), 5); // $ range=>=300
range(y5); // y6 >= 0
}
range(y1 + y2 + y3 + y4 + y5); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5;
range(y1 + y2 + y3 + y4 + y5); // $ overflow=+ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5; // $ overflow=+
}
// Test the comma expression.
@@ -640,15 +640,15 @@ unsigned int test_comma01(unsigned int x) {
unsigned int y1;
unsigned int y2;
y1 = (++y, y);
range(y1); // $ MISSING:range="==... ? ... : ...+1"
range(y1); // $ range="==... ? ... : ...+1"
y2 = (y++,
range(y), // $ MISSING:range="==++ ...:... = ...+1" MISSING:range="==... ? ... : ...+2"
range(y), // $ range="==++ ...:... = ...+1" range="==... ? ... : ...+2"
y += 3,
range(y), // $ MISSING:range="==++ ...:... = ...+4" MISSING:range="==... +++3" range="==... ? ... : ...+5"
range(y), // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
y);
range(y2); // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
range(y1 + y2); // $ MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
return y1 + y2;
range(y1 + y2); // $ overflow=+ MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
return y1 + y2; // $ overflow=+
}
void test17() {
@@ -692,7 +692,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
range(b); // $ range=<=23 range=>=0
int r = a*b; // 0 .. 253
range(r);
total += r;
total += r; // $ overflow=+
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
}
if (3 <= a && a <= 11 && 13 <= b && b <= 23) {
@@ -700,7 +700,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
range(b); // $ range=<=23 range=>=13
int r = a*b; // 39 .. 253
range(r);
total += r;
total += r; // $ overflow=+
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
}
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
@@ -721,14 +721,14 @@ int test_unsigned_mult02(unsigned b) {
range(b); // $ range=<=23 range=>=0
int r = 11*b; // 0 .. 253
range(r);
total += r;
total += r; // $ overflow=+
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
}
if (13 <= b && b <= 23) {
range(b); // $ range=<=23 range=>=13
int r = 11*b; // 143 .. 253
range(r);
total += r;
total += r; // $ overflow=+
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
}
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
@@ -751,7 +751,7 @@ unsigned long mult_overflow() {
range(x); // $ range===274177
y = 67280421310721UL;
range(y);
xy = x * y;
xy = x * y; // $ overflow=+-
range(xy);
return xy; // BUG: upper bound should be >= 18446744073709551617UL
}
@@ -760,14 +760,14 @@ unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
if (ui >= 10) {
range(ui); // $ range=>=10
range((unsigned long)ui); // $ range=>=10
unsigned long result = (unsigned long)ui * ui;
range(result); // $ range=>=100 range=>=100
unsigned long result = (unsigned long)ui * ui; // $ overflow=+
range(result); // $ MISSING: range=>=100
return result; // BUG: upper bound should be >= 18446744065119617025
}
if (ul >= 10) {
range(ul); // $ range=>=10
unsigned long result = ul * ul;
range(result); // $ range=>=100
unsigned long result = ul * ul; // $ overflow=+
range(result); // $ MISSING: range=>=100
return result; // BUG: lower bound should be 0 (overflow is possible)
}
return 0;
@@ -800,13 +800,13 @@ int mul_by_constant(int i, int j) {
i = 5 * i;
range(i); // $ range=<=10 range=>=-5
i = i * -3;
i = i * -3; // $ overflow=+-
range(i); // -30 .. 15
i *= 7;
i *= 7; // $ overflow=+-
range(i); // -210 .. 105
i *= -11;
i *= -11; // $ overflow=+-
range(i); // -1155 .. 2310
}
if (i == -1) {
@@ -815,7 +815,7 @@ int mul_by_constant(int i, int j) {
i = i * (int)0xffFFffFF; // fully converted literal is -1
range(i); // $ range===1
}
i = i * -1;
i = i * -1; // $ overflow=+-
range( i); // -2^31 .. 2^31-1
signed char sc = 1;
@@ -851,7 +851,7 @@ int notequal_type_endpoint(unsigned n) {
n--; // 1 ..
}
range(n); // $ MISSING:range=<=n+0 // 0 .. 0
range(n); // $ range=<=n+0 // 0 .. 0
}
void notequal_refinement(short n) {
@@ -888,7 +888,7 @@ void notequal_variations(short n, float f) {
}
if (n >= 5) {
if (2 * n - 10 == 0) { // Same as `n == 10/2` (modulo overflow)
if (2 * n - 10 == 0) { // $ overflow=+ Same as `n == 10/2` (modulo overflow)
range(n); // $ range=>=5 MISSING: range===5
return;
}
@@ -921,7 +921,7 @@ void two_bounds_from_one_test(short ss, unsigned short us) {
}
if (ss < 0x8001) { // Lower bound removed in `getDefLowerBounds`
range(ss); // $ range=<=32768 MISSING: range=>=-32768
range(ss); // $ overflow=+ range=<=32768 MISSING: range=>=-32768
}
if ((short)us >= 0) {
@@ -936,7 +936,7 @@ void two_bounds_from_one_test(short ss, unsigned short us) {
range(ss); // -32768 .. 32767
}
if (ss + 1 < sizeof(int)) {
if (ss + 1 < sizeof(int)) { // $ overflow=+
range(ss); // -1 .. 2
}
}
@@ -944,7 +944,7 @@ void two_bounds_from_one_test(short ss, unsigned short us) {
void widen_recursive_expr() {
int s;
for (s = 0; s < 10; s++) {
range(s); // $ range=<=9 MISSING:range=>=0
range(s); // $ range=<=9 range=>=0
int result = s + s;
range(result); // $ range=<=18 range=<=s+9 range=>=0 range=>=s+0
}
@@ -1020,7 +1020,7 @@ void test_overflow() {
void test_negate_unsigned(unsigned u) {
if(10 < u && u < 20) {
range<unsigned>(-u); // underflows
range<unsigned>(-u); // $ overflow=-
}
}

View File

@@ -6,17 +6,17 @@
return x;
}
if (y - 2 == x && y > 300) {
if (y - 2 == x && y > 300) { // $ overflow=-
range(x + y); // $ range=<=802 range=>=600
return x + y;
}
if (x != y + 1) {
if (x != y + 1) { // $ overflow=+
range(x); // $ range=<=400
int sum = x + y;
int sum = x + y; // $ overflow=+-
} else {
if (y > 300) {
range(x); // $ range=>=302 range=<=400 range===y+1
range(x); // $ range=>=302 range=<=400 range=<=y+1 MISSING: range===y+1
range(y); // $ range=>=301 range=<=399 range===x-1
int sum = x + y;
}
@@ -38,10 +38,10 @@
return x;
}
if (y == x - 1 && y > 300 && y + 2 == z && z == 350) {
if (y == x - 1 && y > 300 && y + 2 == z && z == 350) { // $ overflow=+ overflow=-
range(x); // $ range===349 range===y+1 range===z-1
range(y); // $ range===348 range===x-1 range===z-2
range(z); // $ range===350 range===x+1 range===y+2
range(y); // $ range===348 range=>=x-1 range===z-2 MISSING: range===x-1
range(z); // $ range===350 range=<=y+2 MISSING: range===x+1 range===y+2
return x + y + z;
}
}