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

Sun Apr 19 13:53:31 PDT 2020

steakhal added a comment.

In D78457#1991288 <https://reviews.llvm.org/D78457#1991288>, @xazax.hun wrote:

> > As turned out we don't even need a BugReporterVisitor for doing the crosscheck.
> >  We should simply use the constraints of the ErrorNode since that has all the necessary information.
>
> This should not be true. But we should definitely have a test case that proves this. The main idea is that unused symbols can be garbage collected. The problem is that the ErrorNode does not have any information about the symbols that were garbage collected earlier. This is why we need the visitor.

You might be right. Could you give a short example to a garbage-collected symbol?
Either way, we need to fix the bug which I stated earlier.

I tried to create a unit-test for the bug, but I miserably failed.
To call the `visitor::finalizeVisitor` you would need almost the entire world.  (A `ExprEngine`, a `CompilerInstance`, etc.)
I also considered a `lit-test`, though I really doubt that is the right tool for testing this.
Since we are constantly improving the checkers, we should not bake in a false-positive bugreport which is then invalidated by the Z3 visitor...

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78457