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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov requested changes to this revision.
george.karpenkov added a comment.
This revision now requires changes to proceed.

> I updated the test case as the cross check is not marking the true bug as invalid anymore.

Awesome! Does it mean that the optimization for adding less constraints was in fact buggy?

> My make clang-test is still failing Driver/response-file.c whenever I compile clang with Z3. I'll update the patch as soon as I find the reason why.



1. You shouldn't use `make`, use `ninja` (also make sure you use `gold` linker, default linker takes forever on Linux)
2. Could it be something unrelated to your changes? Any given trunk version can be buggy, but usually those are resolved very fast, so if you update now the issue can go away.

Watching cfe-commits mailing list might be helpful there.

Otherwise looks good apart from minor naming nit! I guess we could figure out the casting issue later.



================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2360
+static bool
+check_constraints(BugReporterContext &BRC,
+                  const llvm::SmallVector<ConstraintRangeTy, 32> &Cs) {
----------------
we would need a more descriptive name, e.g. `isUnfeasible` or similar.
from `bool check_constraints` it's unclear when `false` is returned.


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2366
+
+  SMTConstraintManager *SMTRefutationMgr =
+      static_cast<SMTConstraintManager*>(RefutationMgr.get());
----------------
mikhail.ramalho wrote:
> I'm not happy about this cast. Suggestions are welcome.
well yeah, `CreateZ3ConstraintManager` should return an `SMTConstraintManager`.
I don't fully understand the problem there, I'll try to take a look.


https://reviews.llvm.org/D45517