[all-commits] [llvm/llvm-project] de361d: [analyzer][Z3-refutation] Fix a refutation BugRepo...

[Balazs Benics via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: de361df3f6d0f20bf16a8deb9e6219556d028b81
      https://github.com/llvm/llvm-project/commit/de361df3f6d0f20bf16a8deb9e6219556d028b81
  Author: Balazs Benics <benicsbalazs at gmail.com>
  Date:   2020-06-29 (Mon, 29 Jun 2020)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
    M clang/lib/StaticAnalyzer/Core/BugReporter.cpp
    M clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
    M clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp

  Log Message:
  -----------
  [analyzer][Z3-refutation] Fix a refutation BugReporterVisitor bug

FalsePositiveRefutationBRVisitor had a bug where the constraints were not
properly collected thus crosschecked with Z3.
This patch demonstratest and fixes that bug.

Bug:
The visitor wanted to collect all the constraints on a BugPath.
Since it is a visitor, it stated the visitation of the BugPath with the node
before the ErrorNode. As a final step, it visited the ErrorNode explicitly,
before it processed the collected constraints.

In principle, the ErrorNode should have visited before every other node.
Since the constraints were collected into a map, mapping each symbol to its
RangeSet, if the map already had a mapping with the symbol, then it was skipped.

This behavior was flawed if:
We already had a constraint on a symbol, but at the end in the ErrorNode we have
a tighter constraint on that. Therefore, this visitor would not utilize that
tighter constraint during the crosscheck validation.

Differential Revision: https://reviews.llvm.org/D78457