[PATCH] D78457: [analyzer][Z3-refutation] Fix refutation BugReporterVisitor bug and refactor

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In D78457#1991780 <https://reviews.llvm.org/D78457#1991780>, @martong wrote:

> If a symbol is unused and garbage collected then that is not part of the path constraint that leads to the ErrorNode, is it? So why should we care about constraints on an unused symbol?


Unused means it is unused at a program point.
For example:

  void f(int sym1, int sym2) {
    int sym3 = sym1 * sym2;
    if (!sym1)
      return;
    // Here sym1 is no longer used, it is garbage collected from the state.
    if (sym3) {
      sym2 / 0; // This is a false positive. sym1 is 0 -> sym3 should be 0 as well, this branch is never taken. But to refute this path we need the info about sym1, that is not available in the ErrorNode state. It was garbage collected earlier.
    } 
  }

I did not try this specific example. The constraint manager might be smart enough to not to report a false positive, but I hope it makes the idea clear why do we need the garbage collected symbols.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D78457/new/

https://reviews.llvm.org/D78457