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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added a comment.

Please resubmit with -U999 diff flag (or using arc)



================
Comment at: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:362
 
+class FalsePositiveRefutationBRVisitor final
+    : public BugReporterVisitorImpl<FalsePositiveRefutationBRVisitor> {
----------------
Can we have the whole class inside the `.cpp` file? It's annoying to recompile half of the analyzer when an internal implementation detail changes


================
Comment at: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:365
+  // Flag first node as seen by the visitor.
+  bool FirstNodeVisited = true;
+
----------------
I'm really not convinced we need this boolean field


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:21
 #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
+#include "llvm/ADT/ImmutableMap.h"
 #include "llvm/ADT/Optional.h"
----------------
NB: diff should be resubmitted with -U999, as phabricator shows "context not available"


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1261
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+    SymbolRef Sym = I.getKey();
----------------
xbolva00 wrote:
> for (auto I : CR)?
@mikhail.ramalho yes please do fix this one


https://reviews.llvm.org/D45517