rnkovacs added inline comments.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249
+bool Z3ConstraintManager::isModelFeasible() {
+ return Solver.check() != Z3_L_FALSE;
+}
----------------
george.karpenkov wrote:
> solver can also return "unknown", what happens then?
If it returns `Z3_L_UNDEF`, e.g. in case of a timeout, this assumes that the
state was feasible because we couldn't prove the opposite. In that case the
report won't be invalidated.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259
+ return;
+ ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
----------------
george.karpenkov wrote:
> TBH I'm really confused here. Why does the method take two constraint ranges?
> What's `OnlyPurged`? From reading the code it seems it's set by seeing
> whether the program point only purges dead symbols, but at least a comment
> should be added as to why this affects behavior.
The logic was:
- add every constraint from the last node (first visited),
- for other nodes on the path, only add those that disappear in the next step.
So `OnlyPurged` is meant to signal that we only want to add those symbols to
the solver that are getting purged from the program state.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1278
+ // a valid APSIntType.
+ if (RangeTy.isNull())
+ continue;
----------------
george.karpenkov wrote:
> I'm really curious where does it happen and why.
I encountered some 1-bit `APSInt`s that wouldn't work together with any other
integer-handling logic. As @ddcc mentioned, he has a fix for that in D35450
(`Z3ConstraintManager::fixAPSInt()`).
https://reviews.llvm.org/D45517
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
