diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll index de93b7bdff3..40183df5bfa 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll @@ -729,7 +729,7 @@ module RangeStage< ) { exists(SemExpr e, D::Delta d1, D::Delta d2 | unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and - boundedUpper(e, b, d1) and + boundedUpper(e, b, d2) and boundedLower(e, b, d2) and delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) ) diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp index df4cd7b4491..2a30caec94d 100644 --- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp +++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp @@ -78,3 +78,36 @@ void testInterproc(BigArray *arr) { 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]; + } + } +}