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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
