]> granicus.if.org Git - clang/commit
[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)
commit040bc2559aa5988618fe601103b4454c835b0f43
treec1b079eec397750155767b920482351ae407909b
parentb264f83ea398d5c0131d7e31c6d814ae7ecd5b72
[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
include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp