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

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2342
+                                            BugReport &BR) {
+  if (isInvalidated)
+    return nullptr;
----------------
george.karpenkov wrote:
> Is this field actually necessary? Do we ever check the same bug report with the same visitor multiple times?
I believe this function is called for each node on the bug path. I have a similar field to indicate the first visited node in the new version, but there may exist a better solution for that as well.


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2351
+
+  if (!RefutationMgr.checkRangedStateConstraints(Succ->getState())) {
+    const LocationContext *LC = Succ->getLocationContext();
----------------
george.karpenkov wrote:
> For the initial version I would just do all work in the visitor, but that's a matter of taste.
I think that doing all the work in the visitor would need exposing even more of `Z3ConstraintManager`'s internals as of `RangedConstraintManager`. I tried to keep such changes minimal.


================
Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:86
+                  ? CreateZ3ConstraintManager(*this, SubEng)
+                  : nullptr;
 }
----------------
george.karpenkov wrote:
> Would then we crash on NPE if `getRefutationManager` is called? Getters should preferably not cause crashes.
Um, currently yes, it will give a backend error if clang isn't built with Z3, but the option is on.


https://reviews.llvm.org/D45517