Home
last modified time | relevance | path

Searched refs:SMTExprRef (Results 1 – 5 of 5) sorted by relevance

/netbsd-src/external/apache2/llvm/dist/llvm/include/llvm/Support/
H A DSMTAPI.h129 using SMTExprRef = const SMTExpr *; variable
178 virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
181 virtual void addConstraint(const SMTExprRef &Exp) const = 0;
184 virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
187 virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
190 virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
193 virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
196 virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
199 virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
202 virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
[all …]
/netbsd-src/external/apache2/llvm/dist/llvm/lib/Support/
H A DZ3Solver.cpp286 void addConstraint(const SMTExprRef &Exp) const override { in addConstraint()
299 SMTExprRef newExprRef(const SMTExpr &Exp) { in newExprRef()
313 SMTSortRef getSort(const SMTExprRef &Exp) override { in getSort()
334 SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { in mkBVNeg()
339 SMTExprRef mkBVNot(const SMTExprRef &Exp) override { in mkBVNot()
344 SMTExprRef mkNot(const SMTExprRef &Exp) override { in mkNot()
349 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAdd()
355 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSub()
361 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVMul()
367 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSRem()
[all …]
/netbsd-src/external/apache2/llvm/dist/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
H A DSMTConv.h39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, in fromUnOp()
41 const llvm::SMTExprRef &Exp) { in fromUnOp()
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, in fromFloatUnOp()
60 const llvm::SMTExprRef &Exp) { in fromFloatUnOp()
74 static inline llvm::SMTExprRef
76 const std::vector<llvm::SMTExprRef> &ASTs) { in fromNBinOp()
82 llvm::SMTExprRef res = ASTs.front(); in fromNBinOp()
90 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, in fromBinOp()
91 const llvm::SMTExprRef &LHS, in fromBinOp()
93 const llvm::SMTExprRef &RHS, in fromBinOp()
[all …]
H A DSMTConstraintManager.h50 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
87 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
88 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
92 llvm::SMTExprRef NotExp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
125 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
140 llvm::SMTExprRef NotExp = SMTConv::fromBinOp( in REGISTER_TRAIT_WITH_PROGRAMSTATE()
298 const llvm::SMTExprRef &Exp) { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
315 std::vector<llvm::SMTExprRef> ASTs; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
317 llvm::SMTExprRef Constraint = I++->second; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
328 const llvm::SMTExprRef &Exp) const { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
/netbsd-src/external/apache2/llvm/dist/clang/lib/StaticAnalyzer/Core/
H A DBugReporterVisitors.cpp2961 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( in finalizeVisitor()