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
