GCC Static Analyzer does not know `a+0 <= b+1` in the true branch of `if (a <= b)`

[Geoffrey1014]

date: 2022-12-29 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)){
       // fact
        __analyzer_eval((a<=b) == true);
        __analyzer_eval((a<b || a==b) == true);

        // Add a positive number
        __analyzer_eval( a+0 <= b+0);

        __analyzer_eval( a+0 <= b+1);
        __analyzer_eval( a+0 < b+1);
        __analyzer_eval( 0 <= 1);

        __analyzer_eval( a+1 <= b+1);
        __analyzer_eval( a+0 <= b+2);
        __analyzer_eval( a+0 < b+2);
        __analyzer_eval( a+1 <= b+2);
        __analyzer_eval( a+1 < b+2);
        __analyzer_eval( a+2 <= b+2);
    }
}

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

[Geoffrey1014]

GCC Static Analyzer does not know "a+0 <= b+1" in the true branch of if (a <= b), but knows "a+0 < b+1".

See it live: https://godbolt.org/z/PGhfKjjWG

Input:

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

int main(int a, int b, int c, int d) {
    if ((a<b)){
       // fact
        __analyzer_eval((a<=b) == true);
        __analyzer_eval((a<b || a==b) == true);

        // Add a positive number
        __analyzer_eval( a+0 <= b+0);

        __analyzer_eval( a+0 <= b+1);
        __analyzer_eval( a+0 < b+1);
        __analyzer_eval( 0 <= 1);

        __analyzer_eval( a+1 <= b+1);
        __analyzer_eval( a+0 <= b+2);
        __analyzer_eval( a+0 < b+2);
        __analyzer_eval( a+1 <= b+2);
        __analyzer_eval( a+1 < b+2);
        __analyzer_eval( a+2 <= b+2);
    }
}

Output:

<source>: In function 'main':
<source>:7:9: warning: implicit declaration of function '__analyzer_eval' [-Wimplicit-function-declaration]
    7 |         __analyzer_eval((a<=b) == true);
      |         ^~~~~~~~~~~~~~~
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval((a<=b) == true);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval((a<b || a==b) == true);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE
   11 |         __analyzer_eval( a+0 <= b+0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:9: warning: UNKNOWN
   13 |         __analyzer_eval( a+0 <= b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: TRUE
   14 |         __analyzer_eval( a+0 < b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: TRUE
   15 |         __analyzer_eval( 0 <= 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:9: warning: TRUE
   17 |         __analyzer_eval( a+1 <= b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:9: warning: UNKNOWN
   18 |         __analyzer_eval( a+0 <= b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:9: warning: UNKNOWN
   19 |         __analyzer_eval( a+0 < b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:20:9: warning: UNKNOWN
   20 |         __analyzer_eval( a+1 <= b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:21:9: warning: TRUE
   21 |         __analyzer_eval( a+1 < b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:22:9: warning: TRUE
   22 |         __analyzer_eval( a+2 <= b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

[Geoffrey1014]

CSA give the similar evaluation result: https://godbolt.org/z/z6o8dzaYK

actually，CSA‘s performance is worse.

[Geoffrey1014]

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

[Geoffrey1014]

more reduced case: https://godbolt.org/z/s7cKfhMfr