]> granicus.if.org Git - clang/commit
[analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and...
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Wed, 25 Jul 2018 12:49:43 +0000 (12:49 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Wed, 25 Jul 2018 12:49:43 +0000 (12:49 +0000)
commit7179078a7a3501a27cc18d911079025a3865e134
treedcd89c08946de89ef824f47b9a552954f9eb8805
parent375087785c80101af6a2c57f4dab1319d07b25ad
[analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver

Summary:
Third patch in the refactoring series, to decouple the SMT Solver from the Refutation Manager (1st: D49668, 2nd: D49767).

The refutation API in the `SMTConstraintManager` was a hack to allow us to create an SMT solver and verify the constraints; it was conceptually wrong from the start. Now, we don't actually need to use the `SMTConstraintManager` and can create an SMT object directly, add the constraints and check them.

While updating the Falsification visitor, I inlined the two functions that were used to collect the constraints and add them to the solver.

As a result of this patch, we could move the SMT API elsewhere and as it's not really dependent on the CSA anymore. Maybe we can create a new dir (utils/smt) for Z3 and future solvers?

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@337922 91177308-0d34-0410-b5e6-96231b3b80d8
include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp