Address review.

cpp/ql/src/experimental/semmle/code/cpp/rangeanalysis/InBoundsPointerDeref.qll

@@ -91,11 +91,14 @@ predicate inBounds(PointerDereferenceInstruction ptrDeref) {
         length instanceof VNLength and
         offset instanceof OpOffset and
         b.getValueNumber() = length.(VNLength).getValueNumber() and
+        // It holds that offset <= length + offsetBoundDelta
         boundedOperand(offset.(OpOffset).getOperand(), b, offsetBoundDelta, /*upper*/ true, _) and
-        // this ensures that offset <= length holds
-        offsetBoundDelta <= 0 and
-        // with that we get that offset + offsetDelta < length offsetBoundDelta + lengthDelta - offsetBoundDelta
+        // it also holds that
         offsetDelta < lengthDelta - offsetBoundDelta
+        // taking both inequalities together we get
+        //    offset <= length + offsetBoundDelta
+        // => offset + offsetDelta <= length + offsetBoundDelta + offsetDelta < length + offsetBoundDelta + lengthDelta - offsetBoundDelta
+        // as required
       )
     )
   )

cpp/ql/test/experimental/library-tests/rangeanalysis/inboundsptr/InBounds.expected

@@ -4,7 +4,9 @@
 | test.cpp:27:13:27:16 | Load: access to array |
 | test.cpp:33:5:33:12 | Store: ... = ... |
 | test.cpp:48:5:48:16 | Store: ... = ... |
-| test.cpp:64:11:64:14 | Load: access to array |
-| test.cpp:68:5:68:12 | Store: ... = ... |
-| test.cpp:70:3:70:11 | Store: ... = ... |
-| test.cpp:74:3:74:18 | Store: ... = ... |
+| test.cpp:61:7:61:14 | Store: ... = ... |
+| test.cpp:70:7:70:14 | Store: ... = ... |
+| test.cpp:81:11:81:14 | Load: access to array |
+| test.cpp:85:5:85:12 | Store: ... = ... |
+| test.cpp:87:3:87:11 | Store: ... = ... |
+| test.cpp:91:3:91:18 | Store: ... = ... |

cpp/ql/test/experimental/library-tests/rangeanalysis/inboundsptr/test.cpp

@@ -51,12 +51,29 @@ void test2(unsigned int count) {
   for(unsigned int i = 0; i < count; ++i) {
     a = (int*) malloc(sizeof(int) * count);
     for (int j = 0; j < count; ++j) {
-      a[j] = 0; // in-bounds TODO not detected
+      a[j] = 0; // in-bounds, but not detected due to RangeAnalysis shortcomings
+    }
+  }
+
+  for(unsigned int i = 0; i < 10; ++i) {
+    a = (int*) malloc(sizeof(int) * i);
+    for (unsigned int j = 0; j < i; ++j) {
+      a[j] = 0; // in-bounds
+    }
+  }
+
+}
+void test3(int count) {
+  for(int i = 0; i < count; ++i) {
+    int * a = (int*) malloc(sizeof(int) * i);
+    for (int j = 0; j < i; ++j) {
+      a[j] = 0; // in-bounds
     }
   }
 }
 
-void test3(unsigned long count) {
+
+void test4(unsigned long count) {
   if (count < 1) {
     return;  
   } 
@@ -74,13 +91,13 @@ void test3(unsigned long count) {
   a[count - 3] = 0; // in-bounds
 }
 
-void test4(unsigned int count) {
+void test5(unsigned int count) {
   int* a = (int*) malloc(sizeof(int) * count);
   a[0] = 0; // unknown, call-site dependant
 }
 
 
-void test5(unsigned int count, bool b) {
+void test6(unsigned int count, bool b) {
   if(count < 4) {
     return;
   }
@@ -96,14 +113,14 @@ void test5(unsigned int count, bool b) {
   a[0] = 0; // unknown
 }
 
-void test6(unsigned int object) {
+void test7(unsigned int object) {
   unsigned int* ptr = &object;
   *ptr = 0; // in-bounds, but needs ArrayLengthAnalysis improvements.
 }
 
-void test7() {
+void test8() {
   void (*foo)(unsigned int);
-  foo = &test6;
+  foo = &test7;
   foo(4); // in-bounds, but needs ArrayLengthAnalysis improvements.
 }