[analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 25 Oct 2018 17:27:42 +0000 (17:27 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 25 Oct 2018 17:27:42 +0000 (17:27 +0000)
commit511c7d0cbe679b176a50ebe41624d588f38f9b57
tree4fdf7bf3d22ee5ff986a5e1427e5b8e8c7af01fe
parent5062532683953336b7703ebf81d759cfe18ad0ca
[analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager

Summary:
This patch moves the last method in `Z3ConstraintManager` to `SMTConstraintManager`: `canReasonAbout()`.

The `canReasonAbout()` method checks if a given `SVal` can be encoded in SMT. I've added a new method to the SMT API to return true if a solver can encode floating-point arithmetics and it was enough to make `canReasonAbout()` solver independent.

As an annoying side-effect, `Z3ConstraintManager` is pretty empty now and only (1) creates the Z3 solver object by calling `CreateZ3Solver()` and (2) instantiates `SMTConstraintManager`. Maybe we can get rid of this class altogether in the future: a `CreateSMTConstraintManager()` method that does (1) and (2) and returns the constraint manager object?

Reviewers: george.karpenkov, NoQ

Reviewed By: george.karpenkov

Subscribers: mehdi_amini, xazax.hun, szepet, a.sidorin, dexonsmith, Szelethus, donat.nagy, dkrupp

Differential Revision: https://reviews.llvm.org/D53694

llvm-svn: 345284
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp