GCC Static Analyzer -- evaluates `__analyzer_eval((!(((0 != b[0]) == p_9) && p_9))==false)` to be FALSE in the true branch of `if ((((0 != b[0]) == p_9) && p_9))`
Opened this issue · 2 comments
Geoffrey1014 commented
date: 2023-1-5
commit: 8c8ca873216387bc26046615c806b96f0345ff9d
args: -O0 -fanalyzer
test:
#include <stdbool.h>
void __analyzer_eval(int a) {}
#include "stdint.h"
static int foo(const int p_9)
{ /* block id: 725 */
int a = 8;
int b[2] ={1,1};
for (int i = 0; i < 2; i++)
{
b[i] = 1;
}
lbl_1710:
if ((((0 != b[0]) == p_9) && p_9))
{ /* block id: 818 */
__analyzer_eval((((0 != b[0]) == p_9) && p_9)==true);
__analyzer_eval((!(((0 != b[0]) == p_9) && p_9))==false);
__analyzer_eval(((!(((0 != b[0]) == p_9)))||(!(p_9)))==false);
__analyzer_eval(((0 != b[0]) == p_9));
__analyzer_eval(p_9);
__analyzer_eval((!(((0 != b[0]) == p_9)))==false);
__analyzer_eval((!(p_9))==false);
__analyzer_eval(((!(((0 != b[0]) == p_9)))&&(p_9))==false);
__analyzer_eval(((((0 != b[0]) == p_9))&&(!(p_9)))==false);
__analyzer_eval(((!(((0 != b[0]) == p_9)))&&(!(p_9)))==false);
__analyzer_eval(true);
__analyzer_eval(((0 != b[0]) == p_9)==true);
__analyzer_eval((((0 != b[0]))!=(p_9))==false);
__analyzer_eval((((0 != b[0]))+0)==((p_9)+0));
__analyzer_eval((((0 != b[0]))+0)<((p_9)+1));
__analyzer_eval((((0 != b[0]))+1)==((p_9)+1));
__analyzer_eval((((0 != b[0]))+0)<((p_9)+2));
__analyzer_eval((((0 != b[0]))+1)<((p_9)+2));
__analyzer_eval((((0 != b[0]))+2)==((p_9)+2));
__analyzer_eval((((0 != b[0]))-0)==((p_9)-0));
__analyzer_eval(true);
for (a = (1); (a != 2); ++a)
{ /* block id: 821 */
if (-1)
{
goto lbl_1710;
}
}
}
return p_9;
}
int main()
{
}
report: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108301
fix:
original:
Geoffrey1014 commented
Hi, I found a problem that GCC Static Analyzer evaluates two contradictory expressions to be true at the same time.
The two contradictory expressions are "__analyzer_eval( ((((0 != b[0]) == p_9))) && (p_9) );" and "__analyzer_eval(! ((((0 != b[0]) == p_9))) && (p_9) );".
https://godbolt.org/z/GYj1oaxqr
Input:
#include <stdbool.h>
#include "stdint.h"
void __analyzer_eval(int a) {}
int foo(const int p_9)
{
int a = 8;
int b[2] ={1,1};
for (int i = 0; i < 2; i++)
{
b[i] = 1;
}
lbl_1710:
if ((((0 != b[0]) == p_9) && p_9))
{
__analyzer_eval( ((((0 != b[0]) == p_9))) && (p_9) );
__analyzer_eval(! ((((0 != b[0]) == p_9))) && (p_9) );
for (a = (1); (a != 2); ++a)
{
if (-1)
{
goto lbl_1710;
}
}
}
return p_9;
}
int main(){}
Output:
<source>: In function 'foo':
<source>:18:5: warning: TRUE
18 | __analyzer_eval( ((((0 != b[0]) == p_9))) && (p_9) );
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:5: warning: TRUE
19 | __analyzer_eval(! ((((0 != b[0]) == p_9))) && (p_9) );
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:5: warning: UNKNOWN
18 | __analyzer_eval( ((((0 != b[0]) == p_9))) && (p_9) );
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:5: warning: UNKNOWN
19 | __analyzer_eval(! ((((0 != b[0]) == p_9))) && (p_9) );
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0
Deleted user commented
CSA can handle: https://godbolt.org/z/1Geac3n83