GSA evaluates `e == d + 1` to be UNKNOWN with the fact that `e == d`
Opened this issue · 3 comments
0-0x41 commented
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 commented
See it live: https://godbolt.org/z/Wcd4T1jGa.
Geoffrey1014 commented
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 commented
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);
}
}