[PATCH] D45517: [analyzer] False positive refutation with Z3
Mikhail Ramalho via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Thu May 31 17:02:17 PDT 2018
mikhail.ramalho 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) {}
----------------
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?
https://reviews.llvm.org/D45517
More information about the cfe-commits
mailing list