Home
last modified time | relevance | path

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

/freebsd/contrib/llvm-project/llvm/include/llvm/Support/
H A DSMTAPI.h142 using SMTExprRef = const SMTExpr *; variable
191 virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
194 virtual void addConstraint(const SMTExprRef &Exp) const = 0;
197 virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
200 virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
203 virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
206 virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
209 virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
212 virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
215 virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
[all …]
/freebsd/contrib/llvm-project/llvm/lib/Support/
H A DZ3Solver.cpp300 void addConstraint(const SMTExprRef &Exp) const override { in addConstraint()
313 SMTExprRef newExprRef(const SMTExpr &Exp) { in newExprRef()
327 SMTSortRef getSort(const SMTExprRef &Exp) override { in getSort()
348 SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { in mkBVNeg()
353 SMTExprRef mkBVNot(const SMTExprRef &Exp) override { in mkBVNot()
358 SMTExprRef mkNot(const SMTExprRef &Exp) override { in mkNot()
363 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAdd()
369 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSub()
375 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVMul()
381 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSRem()
[all …]
/freebsd/contrib/llvm-project/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.h54 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
91 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
92 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
96 llvm::SMTExprRef NotExp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
129 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
144 llvm::SMTExprRef NotExp = SMTConv::fromBinOp( in REGISTER_TRAIT_WITH_PROGRAMSTATE()
302 const llvm::SMTExprRef &Exp) { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
319 std::vector<llvm::SMTExprRef> ASTs; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
321 llvm::SMTExprRef Constraint = I++->second; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
332 const llvm::SMTExprRef &Exp) const { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
/freebsd/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/
H A DZ3CrosscheckVisitor.cpp68 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( in finalizeVisitor()