CSA evaluates `(255UL == b) == true` to be FALSE with the fact that `255UL == b`

[Geoffrey1014]

date: 2023-1-10 commit: args: --analyze -Xclang -analyzer-stats -Xclang -analyzer-checker=core,debug.ExprInspection test:

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

void clang_analyzer_eval();

int32_t a(int8_t b) {
  if (255UL == b) {
    clang_analyzer_eval((255UL == b));
    clang_analyzer_eval((255UL == b)==true);
    clang_analyzer_eval(((255UL)!=(b))==false);
    clang_analyzer_eval(((255UL)+0)==((b)+0));
    clang_analyzer_eval(((255UL)-0)==((b)-0));

  }
}

report: https://github.com/llvm/llvm-project/issues/60042 fix: original:

[Geoffrey1014]

Hi, I found a problem that CSA evaluates (255UL == b)==true to be FALSE with the fact that 255UL == b.

https://godbolt.org/z/TEvrav6ja

Input:

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

void clang_analyzer_eval();

int32_t a(int8_t b) {
  if (255UL == b) {
    clang_analyzer_eval((255UL == b));
    clang_analyzer_eval((255UL == b)==true);
    clang_analyzer_eval(((255UL)!=(b))==false);
    clang_analyzer_eval(((255UL)+0)==((b)+0));
    clang_analyzer_eval(((255UL)-0)==((b)-0));

  }
}

Output:

<source>:9:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval((255UL == b));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:10:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval((255UL == b)==true);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval(((255UL)!=(b))==false);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval(((255UL)+0)==((b)+0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval(((255UL)-0)==((b)-0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
===-------------------------------------------------------------------------===
                                Analyzer timers
===-------------------------------------------------------------------------===
  Total Execution Time: 0.0013 seconds (0.0013 wall clock)

   ---User Time---   --System Time--   --User+System--   ---Wall Time---  --- Name ---
   0.0008 ( 65.8%)   0.0000 (  0.0%)   0.0008 ( 64.2%)   0.0009 ( 65.6%)  Path exploration time
   0.0003 ( 23.9%)   0.0000 (  0.0%)   0.0003 ( 23.3%)   0.0003 ( 22.3%)  Path-sensitive report post-processing time
   0.0001 ( 10.3%)   0.0000 (100.0%)   0.0002 ( 12.5%)   0.0002 ( 12.1%)  Syntax-based analysis time
   0.0012 (100.0%)   0.0000 (100.0%)   0.0013 (100.0%)   0.0013 (100.0%)  Total

5 warnings generated.
Compiler returned: 0

[ghost]

Clang Static Analyzer could solve it with -Xanalyzer -analyzer-constraints=z3.