[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 148969.
mikhail.ramalho marked 6 inline comments as done.
mikhail.ramalho added a comment.

1. Moved FalsePositiveRefutationBRVisitor::Profile definition to BugReporterVisitor.cpp
2. Update test cases two run twice, with and without the crosscheck
3. Removed the FirstNodeVisited flag (the solver is being reset after checking the bug reachability)
4. Use ranged loop when adding the constraints


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/analyzer-config.c
  test/Analysis/analyzer-config.cpp
  test/Analysis/z3-crosscheck.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D45517.148969.patch
Type: text/x-patch
Size: 14653 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180529/ee76d19f/attachment-0001.bin>