CSA does not know "b > 0" under the if condition that "a>0 && b > a"

[Geoffrey1014]

date: 2023-03-14
commit: 0c0681b7414c385d0fd5fad302c0d48607262050
args: --analyze -Xclang -analyzer-stats -Xclang -analyzer-checker=core,debug.ExprInspection
test:

#include <stdint.h>
#include <stdbool.h>
void clang_analyzer_eval();

int foo(int a, int b) {
    if ((a<b) && (0 < a)){
        clang_analyzer_eval(!(a<b) == false); 
        clang_analyzer_eval(b > 0);
    }
}

report: llvm/llvm-project#61511
fix:
original:

[Geoffrey1014]

CSA does not know "b > 0" under the if condition that "a>0 && b > a"

Compiler options: --analyze -Xclang -analyzer-constraints=range --analyzer-output text -Xclang -analyzer-display-progress -Xclang -analyzer-checker=core,alpha.core,debug.ExprInspection -Xclang -analyzer-config -Xclang eagerly-assume=false

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

Input:

#include <stdint.h>
#include <stdbool.h>
void clang_analyzer_eval();

int foo(int a, int b) {
    if ((a<b) && (0 < a)){
        clang_analyzer_eval(!(a<b) == false); 
        clang_analyzer_eval(b > 0);
    }
}

Output:

ANALYZE (Syntax): <source> foo : 6.2 ms
ANALYZE (Path,  Inline_Regular): <source> foo : 9.6 ms
<source>:7:9: warning: TRUE [debug.ExprInspection]
        clang_analyzer_eval(!(a<b) == false); 
        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:6:10: note: Assuming 'a' is < 'b'
    if ((a<b) && (0 < a)){
         ^~~
<source>:6:9: note: Left side of '&&' is true
    if ((a<b) && (0 < a)){
        ^
<source>:6:19: note: Assuming 'a' is > 0
    if ((a<b) && (0 < a)){
                  ^~~~~
<source>:6:5: note: Taking true branch
    if ((a<b) && (0 < a)){
    ^
<source>:7:9: note: TRUE
        clang_analyzer_eval(!(a<b) == false); 
        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: UNKNOWN [debug.ExprInspection]
        clang_analyzer_eval(b > 0);
        ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:6:10: note: Assuming 'a' is < 'b'
    if ((a<b) && (0 < a)){
         ^~~
<source>:6:9: note: Left side of '&&' is true
    if ((a<b) && (0 < a)){
        ^
<source>:6:19: note: Assuming 'a' is > 0
    if ((a<b) && (0 < a)){
                  ^~~~~
<source>:6:5: note: Taking true branch
    if ((a<b) && (0 < a)){
    ^
<source>:8:9: note: UNKNOWN
        clang_analyzer_eval(b > 0);
        ^~~~~~~~~~~~~~~~~~~~~~~~~~
===-------------------------------------------------------------------------===
                                Analyzer timers
===-------------------------------------------------------------------------===
  Total Execution Time: 0.0016 seconds (0.0170 wall clock)

   --System Time--   --User+System--   ---Wall Time---  --- Name ---
   0.0010 ( 62.5%)   0.0010 ( 62.5%)   0.0096 ( 56.4%)  Path exploration time
   0.0005 ( 28.7%)   0.0005 ( 28.7%)   0.0073 ( 42.7%)  Syntax-based analysis time
   0.0001 (  8.9%)   0.0001 (  8.9%)   0.0001 (  0.8%)  Path-sensitive report post-processing time
   0.0016 (100.0%)   0.0016 (100.0%)   0.0170 (100.0%)  Total

2 warnings generated.
Compiler returned: 0

[Deleted user]

GSA (with -O0、-O1、-O2、-O3) does not know "b > 0" under the if condition that "a>0 && b > a": https://godbolt.org/z/M3KGacKP1.