[Bug analyzer/108598] GCC analyzer reports false positive for buffer overflow/over-read in C code with a write in middle of an array.

[psimovec at redhat dot com via Gcc-bugs]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108598

--- Comment #2 from Pavel Šimovec <psimovec at redhat dot com> ---
Thanks for the insightful response.

We agree with the resolution, and I have missed that one of the tools actually
verifies the error:
https://github.com/aufover/aufover-benchmark/blob/77f9432747988bfbfb3a943b246c00904086b234/tests/single-c/arrays-and-loops/reverse-array-bad-0006/output-exp%40symbiotic#L2

It just found the error sooner - already inside the first loop:
for (int i = 0; i < length; i++) {
    arr[i] = __VERIFIER_nondet_int();
}