GCC Static Analyzer does not know `a+3 > b+1` in the true branch of `if (a > b)`

[Geoffrey1014]

date: 2022-12-13 Commit: 8c8ca873216387bc26046615c806b96f0345ff9d args: -O0 -fanalyzer test:

#include <stdint.h>
#include <stdbool.h>

int main(int a, int b, int c, int d) {
    if ((a>b)){
        __analyzer_eval(a>b);
        __analyzer_eval(!(a>b) == false);
        __analyzer_eval(-a < -b);
        __analyzer_eval(0-a < 0-b);
        __analyzer_eval( a+0 > b+0);
        __analyzer_eval( a+1 > b+1);
        __analyzer_eval( a+2 > b+2);
        __analyzer_eval( a+2 > b+1);
        __analyzer_eval( a+3 > b+1);
        __analyzer_eval( a*0 > b*0 == false);
        __analyzer_eval( a*1 > b*1);
        __analyzer_eval( a*2 > b*2);
        __analyzer_eval( a*3 > b*2);
    }
}

report: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109194 fix: original:

[Geoffrey1014]

I found a problem that GCC Static Analyzer does not know "a+3 > b+1" (line 14) in the true branch of "if (a > b) ", but it knows "a+2 > b+1" (line 13) .

I run gcc (trunk) with options -fanalyzer -O0. https://godbolt.org/z/61nMxo7Kv

Input:

#include <stdint.h>
#include <stdbool.h>

int main(int a, int b, int c, int d) {
    if ((a>b)){
        __analyzer_eval(a>b);
        __analyzer_eval(!(a>b) == false);
        __analyzer_eval(-a < -b);
        __analyzer_eval(0-a < 0-b);
        __analyzer_eval( a+0 > b+0);
        __analyzer_eval( a+1 > b+1);
        __analyzer_eval( a+2 > b+2);
        __analyzer_eval( a+2 > b+1);
        __analyzer_eval( a+3 > b+1);
        __analyzer_eval( a*0 > b*0 == false);
        __analyzer_eval( a*1 > b*1);
        __analyzer_eval( a*2 > b*2);
        __analyzer_eval( a*3 > b*2);
    }
}

Output:

<source>: In function 'main':
<source>:6:9: warning: implicit declaration of function '__analyzer_eval' [-Wimplicit-function-declaration]
    6 |         __analyzer_eval(a>b);
      |         ^~~~~~~~~~~~~~~
<source>:6:9: warning: TRUE
    6 |         __analyzer_eval(a>b);
      |         ^~~~~~~~~~~~~~~~~~~~
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval(!(a>b) == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval(-a < -b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:9:9: warning: TRUE
    9 |         __analyzer_eval(0-a < 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:10:9: warning: TRUE
   10 |         __analyzer_eval( a+0 > b+0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE
   11 |         __analyzer_eval( a+1 > b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: TRUE
   12 |         __analyzer_eval( a+2 > b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:9: warning: TRUE
   13 |         __analyzer_eval( a+2 > b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval( a+3 > b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: TRUE
   15 |         __analyzer_eval( a*0 > b*0 == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:9: warning: TRUE
   16 |         __analyzer_eval( a*1 > b*1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:9: warning: TRUE
   17 |         __analyzer_eval( a*2 > b*2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:9: warning: TRUE
   18 |         __analyzer_eval( a*3 > b*2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

[Geoffrey1014]

duplicate of https://github.com/Geoffrey1014/SA_Bugs/issues/24