GSA evaluates `e == d + 1` to be UNKNOWN with the fact that `e == d`

[0-0x41]

date: 2023-2-7 commit: args: -O0 --fanalyzer test:

void __analyzer_eval();
void __analyzer_describe();

void c()
{
    int d[2] = {42,43};
    int *e = d;

    if (e == d)
    {
        __analyzer_describe(0, e);
        __analyzer_describe(0, e + 1);
        __analyzer_describe(0, d + 1);

        __analyzer_eval(e == d + 1);
        __analyzer_eval(e + 1 == d + 1);
    }
}

report: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109736 fix: original:

[0-0x41]

See it live: https://godbolt.org/z/Wcd4T1jGa.

[Geoffrey1014]

Hi, David. I found a problem that GCC Static Analyzer evaluates e == d + 1 to be UNKNOWN with the fact that e == d.
Maybe GCC Static Analyzer should have the ability to evaluates e == d + 1 to be FALSE ?

See it live: https://godbolt.org/z/xKMxzvj6E https://godbolt.org/z/nnnnM5fTM Input:

void __analyzer_eval();
void __analyzer_describe();

void c()
{
    int d[2] = {42,43};
    int *e = d;

    if (e == d)
    {
        __analyzer_describe(0, e);
        __analyzer_describe(0, e + 1);
        __analyzer_describe(0, d + 1);

        __analyzer_eval(e == d + 1);
        __analyzer_eval(e + 1 == d + 1);
    }
}

Output:

<source>: In function 'c':
<source>:11:9: warning: svalue: '&d'
   11 |         __analyzer_describe(0, e);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: svalue: '(&d+(sizetype)4)'
   12 |         __analyzer_describe(0, &d + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval(e == &d + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: TRUE
   15 |         __analyzer_eval(e + 1 == &d + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

[Geoffrey1014]

same case: note d + 2 is UB

void __analyzer_eval();
void __analyzer_describe();

void c()
{
    int d[1] = {10086};
    int *e = d;

    if (e == d)
    {
        __analyzer_describe(0, e);
        __analyzer_describe(0, d + 1); 

        __analyzer_eval(e == d + 1);
        __analyzer_eval(e + 1 == d + 1);
    }
}