GSA evaluates __analyzer_eval((((c) + 1) == ((&b[0]) + 1))) to be FLASE with the fact c == &b[0]

[0-0x41]

date: 2023-1-28
commit: 8c8ca873216387bc26046615c806b96f0345ff9d
args: -O0 -fanalyzer
test:

#include "stdio.h"
void __analyzer_eval();
void __analyzer_dump();

void main()
{
    int *b[1] = {};
    int **c = &b[0];
    if (c == &b[0])
    {
        __analyzer_dump();
        int *p = (int *)0;
        __analyzer_describe(1, c+1);
        __analyzer_describe(1, (&b[0]) + 1);
        __analyzer_eval((((c) + 1) == ((&b[0]) + 1)));
        if (((c) + 1) == ((&b[0]) + 1))
        {
            *p = 42;
        }
    }
}

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

[0-0x41]

GSA evaluates __analyzer_eval((((c) + 1) == ((&b[0]) + 1))) to be FLASE with the fact c == &b[0]. However, the analyzer evaluates both __analyzer_describe(0, c+1); and __analyzer_describe(0, (&b[0]) + 1); to be '(&b[(int)0]+(sizetype)8)'.

See it live:
GSA: https://godbolt.org/z/1sbKEfv43
CSA: https://godbolt.org/z/hzsjPcKh7

Input:

#include "stdio.h"
void __analyzer_eval();
void __analyzer_dump();
void __analyzer_describe();

void main()
{
    int *b[1] = {};
    int **c = &b[0];
    if (c == &b[0])
    {
        __analyzer_dump();
        int *p = (int *)0;
        __analyzer_describe(0, c+1);
        __analyzer_describe(0, (&b[0]) + 1);
        __analyzer_eval((((c) + 1) == ((&b[0]) + 1)));
        if (((c) + 1) == ((&b[0]) + 1))
        {
            *p = 42;
        }
    }
}

Output:

rmodel:
stack depth: 1
  frame (index 0): frame: 'main'@1
clusters within frame: 'main'@1
  cluster for: b: CAST(int *[1], (char)0)
  cluster for: c_8: &b[(int)0]
m_called_unknown_fn: FALSE
constraint_manager:
  equiv classes:
  constraints:
<source>: In function 'main':
<source>:14:9: warning: svalue: '(&b[(int)0]+(sizetype)8)'
   14 |         __analyzer_describe(0, c+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: svalue: '(&b[(int)0]+(sizetype)8)'
   15 |         __analyzer_describe(0, (&b[0]) + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:9: warning: FALSE
   16 |         __analyzer_eval((((c) + 1) == ((&b[0]) + 1)));
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0