Geoffrey1014/SA_Bugs

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