diff options
| author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-07-25 12:49:43 +0000 |
|---|---|---|
| committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-07-25 12:49:43 +0000 |
| commit | 5c3d032e70a8bca7c90092513c216b401477e23d (patch) | |
| tree | 178d3db00bda60cbb54c28ed7256f47ebd44e930 /llvm/lib/CodeGen/AsmPrinter/DwarfStringPool.cpp | |
| parent | 8628e2cd54f11a55155805e575f5378b6b231534 (diff) | |
| download | llvm-5c3d032e70a8bca7c90092513c216b401477e23d.zip llvm-5c3d032e70a8bca7c90092513c216b401477e23d.tar.gz llvm-5c3d032e70a8bca7c90092513c216b401477e23d.tar.bz2 | |
[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
Diffstat (limited to 'llvm/lib/CodeGen/AsmPrinter/DwarfStringPool.cpp')
0 files changed, 0 insertions, 0 deletions