CSA --A false-positive finding by [core.DivideZero] declared to be fixed (but still has some problems) (llvm-project issue #51282)

This original problem (https://github.com/llvm/llvm-project/issues/51282) was decleared to be resolved. However, CSA still reports a wrong NPD warning when analyzing the following program. CSA assumes 'y' is equal to 1, but 'y' should be 0 at that position, which could be computed out. https://godbolt.org/z/ovGxG3roE

void clang_analyzer_printState();
void clang_analyzer_eval(int);
void clang_analyzer_warnIfReached();

void foo(int x, int y) {
  int *a = 0;

  if (x * y != 0) // x * y == 0
    return;

  if (x % 3 == 0) // x % 3 != 0 -> x != 0
    return;
  clang_analyzer_eval(x != 0);
  clang_analyzer_eval( x * y == 0);
  if (y != 1)     // y == 1     -> x == 0
    return;

//   clang_analyzer_eval(x != 0); // this line 会 使 NPD 消失
//   clang_analyzer_eval(y != 0); // this line 不会 使 NPD 消失

  *a = 1;
  clang_analyzer_warnIfReached(); // no-warning
}

Output:

<source>:18:3: warning: TRUE [debug.ExprInspection]
  clang_analyzer_eval(x != 0);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:7: note: Assuming the condition is false
  if (x * y != 0) // x * y == 0
      ^~~~~~~~~~
<source>:13:3: note: Taking false branch
  if (x * y != 0) // x * y == 0
  ^
<source>:16:7: note: Assuming the condition is false
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
      ^~~~~~~~~~
<source>:16:3: note: Taking false branch
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
  ^
<source>:18:23: note: 'x' is not equal to 0
  clang_analyzer_eval(x != 0);
                      ^
<source>:18:3: note: TRUE
  clang_analyzer_eval(x != 0);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:3: warning: TRUE [debug.ExprInspection]
  clang_analyzer_eval( x * y == 0);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:7: note: Assuming the condition is false
  if (x * y != 0) // x * y == 0
      ^~~~~~~~~~
<source>:13:3: note: Taking false branch
  if (x * y != 0) // x * y == 0
  ^
<source>:16:7: note: Assuming the condition is false
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
      ^~~~~~~~~~
<source>:16:3: note: Taking false branch
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
  ^
<source>:18:23: note: 'x' is not equal to 0
  clang_analyzer_eval(x != 0);
                      ^
<source>:19:3: note: TRUE
  clang_analyzer_eval( x * y == 0);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:26:6: warning: Dereference of null pointer (loaded from variable 'a') [core.NullDereference]
  *a = 1;
   ~ ^
<source>:11:3: note: 'a' initialized to a null pointer value
  int *a = 0;
  ^~~~~~
<source>:13:7: note: Assuming the condition is false
  if (x * y != 0) // x * y == 0
      ^~~~~~~~~~
<source>:13:3: note: Taking false branch
  if (x * y != 0) // x * y == 0
  ^
<source>:16:7: note: Assuming the condition is false
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
      ^~~~~~~~~~
<source>:16:3: note: Taking false branch
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
  ^
<source>:18:23: note: 'x' is not equal to 0
  clang_analyzer_eval(x != 0);
                      ^
<source>:20:7: note: Assuming 'y' is equal to 1
  if (y != 1)     // y == 1     -> x == 0
      ^~~~~~
<source>:20:3: note: Taking false branch
  if (y != 1)     // y == 1     -> x == 0
  ^
<source>:26:6: note: Dereference of null pointer (loaded from variable 'a')
  *a = 1;
   ~ ^
3 warnings generated.
Compiler returned: 0

But if i uncomment // clang_analyzer_eval(x != 0);, the NPD false positive report disappear. CSA assumes 'y' is not equal to 1. I do not know why // clang_analyzer_eval(x != 0); can have impact on the assumption of 'y'. https://godbolt.org/z/Kc3d14bzo Input:

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core \
// RUN:   -analyzer-checker=debug.ExprInspection \
// RUN:   -verify

void clang_analyzer_printState();
void clang_analyzer_eval(int);
void clang_analyzer_warnIfReached();

void foo(int x, int y) {
  int *a = 0;

  if (x * y != 0) // x * y == 0
    return;

  if (x % 3 == 0) // x % 3 != 0 -> x != 0
    return;
  clang_analyzer_eval(x != 0);
  clang_analyzer_eval(y != 1);
  if (y != 1)     // y == 1     -> x == 0
    return;

  clang_analyzer_eval(x == 0);
  *a = 1;
  clang_analyzer_warnIfReached(); // no-warning
}

Output:

<source>:18:3: warning: TRUE [debug.ExprInspection]
  clang_analyzer_eval(x != 0);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:7: note: Assuming the condition is false
  if (x * y != 0) // x * y == 0
      ^~~~~~~~~~
<source>:13:3: note: Taking false branch
  if (x * y != 0) // x * y == 0
  ^
<source>:16:7: note: Assuming the condition is false
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
      ^~~~~~~~~~
<source>:16:3: note: Taking false branch
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
  ^
<source>:18:23: note: 'x' is not equal to 0
  clang_analyzer_eval(x != 0);
                      ^
<source>:18:3: note: TRUE
  clang_analyzer_eval(x != 0);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:3: warning: TRUE [debug.ExprInspection]
  clang_analyzer_eval(y != 1);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:7: note: Assuming the condition is false
  if (x * y != 0) // x * y == 0
      ^~~~~~~~~~
<source>:13:3: note: Taking false branch
  if (x * y != 0) // x * y == 0
  ^
<source>:16:7: note: Assuming the condition is false
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
      ^~~~~~~~~~
<source>:16:3: note: Taking false branch
  if (x % 3 == 0) // x % 3 != 0 -> x != 0
  ^
<source>:18:23: note: 'x' is not equal to 0
  clang_analyzer_eval(x != 0);
                      ^
<source>:19:23: note: Assuming 'y' is not equal to 1
  clang_analyzer_eval(y != 1);
                      ^~~~~~
<source>:19:3: note: TRUE
  clang_analyzer_eval(y != 1);
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~
2 warnings generated.
Compiler returned: 0

Geoffrey1014 / SA_Bugs

CSA --A false-positive finding by [core.DivideZero] declared to be fixed (but still has some problems) (llvm-project issue #51282) #15