C++: Do not warn on static buffer overflow using loop counters, if the loop counter has been widened

cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

@@ -1593,6 +1593,14 @@ private module SimpleRangeAnalysisCached {
     result = min([max(getTruncatedUpperBounds(expr)), getGuardedUpperBound(expr)])
   }
 
+  /** Holds if `expr` may have been widened */
+  cached
+  predicate upperBoundMayBeWidened(Expr e) {
+    isRecursiveExpr(e) and
+    // Corresponds to taking max on the RHS
+    not getGuardedUpperBound(e) < getTruncatedUpperBounds(e)
+  }
+
   /**
    * Holds if `expr` has a provably empty range. For example:
    *

cpp/ql/src/Critical/OverflowStatic.ql

@@ -55,6 +55,8 @@ predicate overflowOffsetInLoop(BufferAccess bufaccess, string msg) {
     loop.counter().getAnAccess() = bufaccess.getArrayOffset() and
     // Ensure that we don't have an upper bound on the array index that's less than the buffer size.
     not upperBound(bufaccess.getArrayOffset().getFullyConverted()) < bufaccess.bufferSize() and
+    // The upper bounds analysis must not have been widended
+    not upperBoundMayBeWidened(bufaccess.getArrayOffset().getFullyConverted()) and
     msg =
       "Potential buffer-overflow: counter '" + loop.counter().toString() + "' <= " +
         loop.limit().toString() + " but '" + bufaccess.buffer().getName() + "' has " +