[Bug analyzer/108598] New: 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

            Bug ID: 108598
           Summary: GCC analyzer reports false positive for buffer
                    overflow/over-read in C code with a write in middle of
                    an array.
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: psimovec at redhat dot com
  Target Milestone: ---

In this test case, gcc analyzer found 3 new true positives, but one False
positive. (Compared to analyzer in gcc 12)

It reports an error "write of 4 bytes to beyond the end of the region" with
write in middle of array.

Test case:
#include <stdlib.h>
extern int __VERIFIER_nondet_int(void);
extern char __VERIFIER_nondet_char(void);

int main(void)
{
    int length = 99;

    int *arr = alloca(length);

    for (int i = 0; i < length; i++) {
        arr[i] = __VERIFIER_nondet_int();
    }

    for (int i = 0; i < length; i++) {
        if (arr[i] == '\0')
            arr[i]++;
    }

    arr[length / 2 + 1] = '\0'; // <- false positive here
    int *a = arr;
    int *b = arr + length - 1;
    int tmp;
    while (*a != 0 && *b != 0) {
        tmp = *a;
        *a = *b;
        *b = tmp;
        a++;
        b--;
    }
    return 0;
}

GCC analyzer reported errors:
Error: GCC_ANALYZER_WARNING (CWE-121): <--- False positive
./test-0006.c: scope_hint: In function 'main'
./test-0006.c:20:25: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
overflow
/usr/include/stdlib.h:587: included_from: Included from here.
./test-0006.c:1: included_from: Included from here.
./test-0006.c:20:25: note: write of 4 bytes to beyond the end of the region

Error: GCC_ANALYZER_WARNING (CWE-126): 
./test-0006.c:24:23: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
over-read
./test-0006.c:24:23: note: read of 4 bytes from after the end of the region

Error: GCC_ANALYZER_WARNING (CWE-126):
./test-0006.c:26:14: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
over-read
./test-0006.c:26:14: note: read of 4 bytes from after the end of the region

Error: GCC_ANALYZER_WARNING (CWE-121):
./test-0006.c:27:12: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
overflow
./test-0006.c:27:12: note: write of 4 bytes to beyond the end of the region

---------------------------------------------
gcc (GCC) 13.0.1 20230127 (Red Hat 13.0.1-0)
Fedora release 38 (Rawhide)