george.karpenkov added inline comments.
================ Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183 + virtual void reset() {} + virtual bool isModelFeasible() { return true; } + virtual void addRangeConstraints(ConstraintRangeTy) {} ---------------- mikhail.ramalho wrote: > george.karpenkov wrote: > > Making those virtual does not make much sense to me. > > Returning `true` by default is not correct. > > When we are using the visitor, we should already know we have a > > `Z3ConstraintsManager`, why can't we just use methods of that class? > Z3ConstraintManager is fully contained inside a .cpp file, so we need > isModelFeasible and addRangeConstraints to be exposed via its base class. > > Another solution is to split Z3ConstraintManager into a .h and a .cpp file > and include the header. We would then be able to use it directly, instead of > through a ConstraintManager object. > > I honestly prefer the latter. What do you think? Yeah, I think we would need a header here. In general we try to avoid inheritance and virtual functions unless they are very beneficial, and here they are not. ================ Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391 + if (!RefutationMgr->isModelFeasible()) + BR.markInvalid("Infeasible constraints", N->getLocationContext()); + } ---------------- mikhail.ramalho wrote: > george.karpenkov wrote: > > That would be checking all constraints in all nodes one by one. I thought > > the idea was to encode all constraints from the entire path and then check > > all of it. > All the constraints are being added in the previous for loop, isModelFeasible > only calls check(). Ah right, I see we are inside of the branch when `pred_size() == 0`. Sorry, I was wrong -- but could we move out this code to a private function (could also simply use static function to avoid polluting the header)? https://reviews.llvm.org/D45517 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits