C++: fix equality refinement in new range analysis

This commit is contained in:
Robert Marsh
2023-05-22 11:11:51 -04:00
committed by Robert Marsh
parent 383b2e183d
commit 6a997aba3b
2 changed files with 34 additions and 1 deletions

View File

@@ -729,7 +729,7 @@ module RangeStage<
) { ) {
exists(SemExpr e, D::Delta d1, D::Delta d2 | exists(SemExpr e, D::Delta d1, D::Delta d2 |
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
boundedUpper(e, b, d1) and boundedUpper(e, b, d2) and
boundedLower(e, b, d2) and boundedLower(e, b, d2) and
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
) )

View File

@@ -78,3 +78,36 @@ void testInterproc(BigArray *arr) {
addToPointerAndAssign(arr->buf); addToPointerAndAssign(arr->buf);
} }
void testEqRefinement() {
int arr[MAX_SIZE];
for(int i = 0; i <= MAX_SIZE; i++) {
if(i != MAX_SIZE) {
arr[i] = 0;
}
}
}
void testEqRefinement2() {
int arr[MAX_SIZE];
int n = 0;
for(int i = 0; i <= MAX_SIZE; i++) {
if(n == 0) {
if(i == MAX_SIZE) {
break;
}
n = arr[i];
continue;
}
if (i == MAX_SIZE || n != arr[i]) {
if (i == MAX_SIZE) {
break;
}
n = arr[i];
}
}
}