Searched refs:SMTSolverRef (Results 1 – 5 of 5) sorted by relevance
| /netbsd-src/external/apache2/llvm/dist/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, in mkSort()
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, in fromUnOp()
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, in fromFloatUnOp()
75 fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, in fromNBinOp()
90 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, in fromBinOp()
169 fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, in fromFloatSpecialBinOp()
201 static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, in fromFloatBinOp()
260 static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, in fromCast()
313 static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, in castAPSInt()
323 fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) { in fromData()
[all …]
|
| H A D | SMTConstraintManager.h | 31 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
|
| /netbsd-src/external/apache2/llvm/dist/llvm/include/llvm/Support/ |
| H A D | SMTAPI.h | 440 using SMTSolverRef = std::shared_ptr<SMTSolver>; variable
443 SMTSolverRef CreateZ3Solver();
|
| /netbsd-src/external/apache2/llvm/dist/llvm/lib/Support/ |
| H A D | Z3Solver.cpp | 903 llvm::SMTSolverRef llvm::CreateZ3Solver() { in CreateZ3Solver()
|
| /netbsd-src/external/apache2/llvm/dist/clang/lib/StaticAnalyzer/Core/ |
| H A D | BugReporterVisitors.cpp | 2953 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); in finalizeVisitor()
|