GSA evaluates `__analyzer_eval((((c) + 1) == ((&b[0]) + 1)))` to be FLASE with the fact `c == &b[0]`
Opened this issue · 1 comments
0-0x41 commented
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 commented
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