[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
Loading
Please register or sign in to comment