diff options
| author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-10-25 17:27:42 +0000 |
|---|---|---|
| committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-10-25 17:27:42 +0000 |
| commit | 040bc2559aa5988618fe601103b4454c835b0f43 (patch) | |
| tree | c1b079eec397750155767b920482351ae407909b /test | |
| parent | b264f83ea398d5c0131d7e31c6d814ae7ecd5b72 (diff) | |
[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
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@345284 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions