Home
last modified time | relevance | path

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

/openbsd-src/gnu/llvm/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 …]
/openbsd-src/gnu/llvm/llvm/lib/Support/
H A DZ3Solver.cpp288 void addConstraint(const SMTExprRef &Exp) const override { in addConstraint()
301 SMTExprRef newExprRef(const SMTExpr &Exp) { in newExprRef()
315 SMTSortRef getSort(const SMTExprRef &Exp) override { in getSort()
336 SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { in mkBVNeg()
341 SMTExprRef mkBVNot(const SMTExprRef &Exp) override { in mkBVNot()
346 SMTExprRef mkNot(const SMTExprRef &Exp) override { in mkNot()
351 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAdd()
357 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSub()
363 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVMul()
369 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSRem()
[all …]
/openbsd-src/gnu/llvm/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.h51 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
88 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
89 llvm::SMTExprRef Exp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
93 llvm::SMTExprRef NotExp = in REGISTER_TRAIT_WITH_PROGRAMSTATE()
126 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
141 llvm::SMTExprRef NotExp = SMTConv::fromBinOp( in REGISTER_TRAIT_WITH_PROGRAMSTATE()
299 const llvm::SMTExprRef &Exp) { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
316 std::vector<llvm::SMTExprRef> ASTs; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
318 llvm::SMTExprRef Constraint = I++->second; in REGISTER_TRAIT_WITH_PROGRAMSTATE()
329 const llvm::SMTExprRef &Exp) const { in REGISTER_TRAIT_WITH_PROGRAMSTATE()
/openbsd-src/gnu/llvm/clang/lib/StaticAnalyzer/Core/
H A DBugReporterVisitors.cpp3440 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( in finalizeVisitor()