[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)
commit5c3d032e70a8bca7c90092513c216b401477e23d
tree178d3db00bda60cbb54c28ed7256f47ebd44e930
parent8628e2cd54f11a55155805e575f5378b6b231534
[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

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