https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109199
Bug ID: 109199
Summary: GCC Static Analyzer evaluates `__analyzer_eval((((c) +
1) == ((&b[0]) + 1)))` to be FLASE with the fact `c ==
&b[0]`
Product: gcc
Version: 13.0
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: analyzer
Assignee: dmalcolm at gcc dot gnu.org
Reporter: geoffreydgr at icloud dot com
Target Milestone: ---
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:
```c
#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
```
