False positive in a loop using '!=' instead of '<'

[gh2375]

This is for tracking the remaining warning from https://github.com/NASA-SW-VnV/ikos/issues/27#issuecomment-448387649.

Code:

struct MyStruct
{
    int arr[10] = {};
};

int main(int argc, char * argv[])
{
    MyStruct s;

    return 0;
}

Output:

# Results
test-array.cpp: In function 'MyStruct::MyStruct()':
test-array.cpp:4:16: warning: possible buffer overflow, pointer '{0: &this->arr[0], 1: &(...)[1]}' points to local variable 's' of size 40 bytes
        int arr[10] = {};
                      ^

System:

MSYS2

Version:

79942e6469bbcbe8a9e0acaf651a65cba1653502

[arthaud]

This is a false positive in the constructor of MyStruct.

Here is the equivalent C code:

int main(int argc, char *argv[]) {
  int array[10];
  int* p = &array[0];
  int* q = &array[10];
  for (; p != q; ++p) {
    *p = 0;
  }
  return 0;
}

test.c: In function 'main':
test.c:6:8: warning: possible buffer overflow, could not bound index for access of local variable 'array' of 10 elements
    *p = 0;
       ^

This is a classic problem in abstract interpretation. The widening is aggressive and it infers that 0 <= offset(p) <= +oo, and the narrowing cannot infer the proper bound.

FIY, this code can be proven by rewriting p != q to p < q and using ikos -d=gauge-interval-congruence.

[ivanperez-keera]

Is there anything that can be done about this in the near term? If not, maybe we can close this, mark it as a question, or move it to discussions.