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.h149 using SMTExprRef = const SMTExpr *; variable
200 virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
203 virtual void addConstraint(const SMTExprRef &Exp) const = 0;
206 virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
209 virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
212 virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
215 virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
218 virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
221 virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
224 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.h41 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, in fromUnOp()
43 const llvm::SMTExprRef &Exp) { in fromUnOp()
60 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, in fromFloatUnOp()
62 const llvm::SMTExprRef &Exp) { in fromFloatUnOp()
76 static inline llvm::SMTExprRef
78 const std::vector<llvm::SMTExprRef> &ASTs) { in fromNBinOp()
84 llvm::SMTExprRef res = ASTs.front(); in fromNBinOp()
92 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, in fromBinOp()
93 const llvm::SMTExprRef &LHS, in fromBinOp()
95 const llvm::SMTExprRef &RHS, in fromBinOp()
[all …]
H A DSMTConstraintManager.h55 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
92 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
93 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
97 llvm::SMTExprRef NotExp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
130 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
145 llvm::SMTExprRef NotExp = SMTConv::fromBinOp( in REGISTER_TRAIT_WITH_PROGRAMSTATE()
312 const llvm::SMTExprRef &Exp) { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
329 llvm::SMTExprRef Constraint = I++->second; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
340 const llvm::SMTExprRef &Exp) const { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
/freebsd/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/
H A DZ3CrosscheckVisitor.cpp78 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( in finalizeVisitor()