Searched refs:SMTSolverRef (Results 1 – 5 of 5) sorted by relevance
| /freebsd-12.1/contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 28 static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty, in mkSort()
40 static inline SMTExprRef fromUnOp(SMTSolverRef &Solver, in fromUnOp()
59 static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver, in fromFloatUnOp()
75 static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver, in fromNBinOp()
91 static inline SMTExprRef fromBinOp(SMTSolverRef &Solver, in fromBinOp()
168 fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS, in fromFloatSpecialBinOp()
200 static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver, in fromFloatBinOp()
310 static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver, in castAPSInt()
319 static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, in fromData()
450 static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx,
[all …]
|
| H A D | SMTSolver.h | 295 using SMTSolverRef = std::shared_ptr<SMTSolver>; variable
298 SMTSolverRef CreateZ3Solver();
|
| H A D | SMTConstraintManager.h | 26 SMTSolverRef &Solver;
30 SMTSolverRef &S) in SMTConstraintManager()
|
| /freebsd-12.1/contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/ |
| H A D | Z3ConstraintManager.cpp | 809 SMTSolverRef Solver = CreateZ3Solver();
820 SMTSolverRef clang::ento::CreateZ3Solver() { in CreateZ3Solver()
|
| H A D | BugReporterVisitors.cpp | 2452 SMTSolverRef RefutationSolver = CreateZ3Solver(); in finalizeVisitor()
|