[C] InferBO false positive

[mianowill]

Please make sure your issue is not addressed in the FAQ.

Please include the following information:

• [x] The version of infer from infer --version. v1.1.0
• [x] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc. Ubuntu 22.04, bare metal
• [x] Which command you ran, for example infer -- make. infer -- gcc test.c
• [x] The full output in a paste, for instance a gist. https://gist.github.com/mianowill/4e2ec778d8f4e28af6727170cb2e54cb
• [x] If possible, a minimal example to reproduce your problem (for instance, some code where infer reports incorrectly, together with the way you run infer to reproduce the incorrect report).

I initially ran into this issue running infer run --compilation-database build/compile_commands.json on a CMake project, and created a small demo file to verify. There's an array which contains a pointer to an array we want to iterate through, and a size_t of the size of the array, such as

lookup_array = {
  [FOO] = {
    .array_size = sizeof(bar) / sizeof(bar[0]), 
    .array_ptr = &bar[0]
  },
  ...
}

Given two inputs x and y, the code checks to see if y is present in the array at lookup_array[x].array_ptr.

bool function(data_t x, data_t y) {
    for (size_t i = 0; i < lookup_array[x].array_size; i++) {
        if (lookup_array[x].array_ptr[i] == y) {
            return true;
        }
    }

    return false;
}

The for-loop will iterate exactly once for each element in the array, given .array_size = sizeof(bar) / sizeof(bar[0]), however Infer believes the loop to iterate as many times as the number of elements of the largest array; that is, if we have an array of size 2 and an array of size 4, it will incorrectly deduce that the array of size 2 will be accessed with offset [0,3] and overrun at size 2.