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

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2871
+      // Overwrite the associated constraint of the Symbol.
+      Constraints = CF.remove(Constraints, Sym);
       Constraints = CF.add(Constraints, Sym, C.second);
----------------
martong wrote:
> steakhal wrote:
> > How can we simplify this?
> Could we change the visitation logic to start with the `EndPathNode`? I mean could we exercise `FalsePositiveRefutationBRVisitor` to start the visitation from `EndPathNode`? If that was possible then this whole patch would be way simpler.
> In BugReporter.cpp:
> ```
>   // Run visitors on all nodes starting from the node *before* the last one.
>   // The last node is reserved for notes generated with {@code getEndPath}.
>   const ExplodedNode *NextNode = ErrorNode->getFirstPred();
>   while (NextNode) {
> ```
> Why can't we have a different visitation order implemented specifically for the refutation visitor? (@NoQ, @xazax.hun)
Hmm, to answer my own question, then we would visit the ErrorNode twice. So then perhaps we should not allow any constraints in the ErrorNodes, right? What if we'd split all such ErrorNodes into a PrevNode with the constraints and a simple ErrorNode without the constraints?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78457