]> granicus.if.org Git - clang/commit
Generalised the SMT state constraints
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 7 Feb 2019 03:17:36 +0000 (03:17 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 7 Feb 2019 03:17:36 +0000 (03:17 +0000)
commit617fd0c671765052789f8c1409d227fe56ee3199
treec0481eae704c634c2d9a98f1a6b1bdfca158c6f8
parent6d763e31d26e7757e5434188a2125763e59cd9e1
Generalised the SMT state constraints

This patch moves the ConstraintSMT definition to the SMTConstraintManager header to make it easier to move the Z3 backend around.

We achieve this by not using shared_ptr  anymore, as llvm::ImmutableSet doesn't seem to like it.

The solver specific exprs and sorts are cached in the Z3Solver object now and we move pointers to those objects around.

As a nice side-effect, SMTConstraintManager doesn't have to be a template anymore. Yay!

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

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