Home
last modified time | relevance | path

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

/freebsd-14.2/contrib/llvm-project/llvm/include/llvm/Support/
H A DSMTAPI.h184 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;
205 virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
220 virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
223 virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
226 virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
229 virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
259 virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
262 virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
[all …]
/freebsd-14.2/contrib/llvm-project/llvm/lib/Support/
H A DZ3Solver.cpp351 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()
393 SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVShl()
411 SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVXor()
417 SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVOr()
423 SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAnd()
429 SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUlt()
477 SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkAnd()
482 SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkOr()
[all …]
/freebsd-14.2/contrib/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
H A DSMTConv.h74 static inline llvm::SMTExprRef
390 llvm::SMTExprRef LHS = in getSymBinExpr()
394 llvm::SMTExprRef RHS = in getSymBinExpr()
402 llvm::SMTExprRef LHS = in getSymBinExpr()
404 llvm::SMTExprRef RHS = in getSymBinExpr()
410 llvm::SMTExprRef LHS = in getSymBinExpr()
412 llvm::SMTExprRef RHS = in getSymBinExpr()
438 llvm::SMTExprRef Exp = in getSymExpr()
474 llvm::SMTExprRef Exp = in getSymExpr()
553 llvm::SMTExprRef ToExp = in getRangeExpr()
[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()
/freebsd-14.2/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/
H A DBugReporterVisitors.cpp3458 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( in finalizeVisitor()