[llvm-bugs] [Bug 51541] New: [Analyzer][solver] Reachable infeasible state

[via llvm-bugs]

https://bugs.llvm.org/show_bug.cgi?id=51541

            Bug ID: 51541
           Summary: [Analyzer][solver] Reachable infeasible state
           Product: clang
           Version: trunk
          Hardware: All
                OS: All
            Status: NEW
          Severity: normal
          Priority: P
         Component: Static Analyzer
          Assignee: dcoughlin at apple.com
          Reporter: martongabesz at gmail.com
                CC: dcoughlin at apple.com, llvm-bugs at lists.llvm.org

Created attachment 25172
  --> https://bugs.llvm.org/attachment.cgi?id=25172&action=edit
lit test file

We reach an infeasible state in the below case. I'm attaching also the lit test
file (solver-x.c) that fails/crashes. My guess is that the solver probably
handles `-=` wrongly.

```
int a, b, c, d, e;
void f() {

  if (a == 0)
    return;

  if (e != c)
    return;

  d = e - c;
  b = d;
  a -= d;

  if (a != 0)
    return;

  clang_analyzer_warnIfReached(); // no-warning

  // Crashes with expensive checks.
  if (b > 0)
    return;
}

```

-- 
You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20210819/03efbae9/attachment-0001.html>