reference, declaration → definition definition → references, declarations, derived classes, virtual overrides reference to multiple definitions → definitions unreferenced |
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; 184 virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 184 virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 187 virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 187 virtual SMTExprRef mkBVSub(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; 190 virtual SMTExprRef mkBVMul(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; 193 virtual SMTExprRef mkBVSRem(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; 196 virtual SMTExprRef mkBVURem(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; 199 virtual SMTExprRef mkBVSDiv(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; 202 virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 202 virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 205 virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 205 virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 205 virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 208 virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 208 virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 208 virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 211 virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 211 virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 211 virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 214 virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0; 214 virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0; 217 virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0; 217 virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0; 220 virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 220 virtual SMTExprRef mkBVXor(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; 223 virtual SMTExprRef mkBVOr(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; 226 virtual SMTExprRef mkBVAnd(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; 229 virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 229 virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 232 virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 232 virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 232 virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 235 virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 235 virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 235 virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 238 virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 238 virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 238 virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 241 virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 241 virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 241 virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 244 virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 244 virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 244 virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 247 virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 247 virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 247 virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 250 virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 250 virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 250 virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 253 virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0; 253 virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0; 256 virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 256 virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 256 virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 259 virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 259 virtual SMTExprRef mkAnd(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; 262 virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 262 virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, 266 const SMTExprRef &F) = 0; 269 virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0; 269 virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0; 272 virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0; 272 virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0; 275 virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, 276 const SMTExprRef &Exp) = 0; 279 virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, 279 virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, 280 const SMTExprRef &RHS) = 0; 284 virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, 284 virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, 285 const SMTExprRef &RHS, 290 virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, 290 virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, 291 const SMTExprRef &RHS) = 0; 295 virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, 295 virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, 296 const SMTExprRef &RHS) = 0; 300 virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, 300 virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, 301 const SMTExprRef &RHS, 306 virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, 306 virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, 307 const SMTExprRef &RHS) = 0; 311 virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0; 311 virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0; 315 virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, 315 virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, 316 const SMTExprRef &RHS, 321 virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, 321 virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, 322 const SMTExprRef &RHS) = 0; 325 virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; 325 virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; 328 virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0; 328 virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0; 331 virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0; 331 virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0; 334 virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0; 334 virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0; 337 virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0; 337 virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0; 340 virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 340 virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 340 virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 343 virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 343 virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 343 virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 346 virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 346 virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 346 virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 349 virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 349 virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 349 virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 352 virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 352 virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 352 virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 355 virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 355 virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 355 virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 358 virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 358 virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 358 virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 361 virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 361 virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 361 virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 364 virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 364 virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 364 virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; 367 virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, 367 virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, 368 const SMTExprRef &RHS) = 0; 372 virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; 372 virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; 376 virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, 376 virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, 381 virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, 381 virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, 386 virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0; 386 virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0; 390 virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0; 390 virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0; 393 virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0; 396 virtual SMTExprRef getFloatRoundingMode() = 0; 399 virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, 403 virtual bool getBoolean(const SMTExprRef &Exp) = 0; 406 virtual SMTExprRef mkBoolean(const bool b) = 0; 409 virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0; 412 virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0; 415 virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0; 418 virtual bool getInterpretation(const SMTExprRef &Exp,tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
48 llvm::SMTExprRef Exp = 85 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); 86 llvm::SMTExprRef Exp = 90 llvm::SMTExprRef NotExp = 123 llvm::SMTExprRef Exp = 139 llvm::SMTExprRef NotExp = SMTConv::fromBinOp( 297 const llvm::SMTExprRef &Exp) { 314 std::vector<llvm::SMTExprRef> ASTs; 316 llvm::SMTExprRef Constraint = I++->second; 327 const llvm::SMTExprRef &Exp) const {tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, 41 const llvm::SMTExprRef &Exp) { 58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, 60 const llvm::SMTExprRef &Exp) { 74 static inline llvm::SMTExprRef 76 const std::vector<llvm::SMTExprRef> &ASTs) { 82 llvm::SMTExprRef res = ASTs.front(); 90 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, 91 const llvm::SMTExprRef &LHS, 93 const llvm::SMTExprRef &RHS, 168 static inline llvm::SMTExprRef 169 fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, 201 static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, 202 const llvm::SMTExprRef &LHS, 204 const llvm::SMTExprRef &RHS) { 260 static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, 261 const llvm::SMTExprRef &Exp, 322 static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, 330 static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, 332 const llvm::SMTExprRef &Exp, 340 static inline llvm::SMTExprRef 342 const llvm::SMTExprRef &LHS, QualType LTy, 343 BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, 345 llvm::SMTExprRef NewLHS = LHS; 346 llvm::SMTExprRef NewRHS = RHS; 376 static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, 385 llvm::SMTExprRef LHS = 389 llvm::SMTExprRef RHS = 397 llvm::SMTExprRef LHS = 399 llvm::SMTExprRef RHS = 405 llvm::SMTExprRef LHS = 407 llvm::SMTExprRef RHS = 417 static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, 434 llvm::SMTExprRef Exp = 446 llvm::SMTExprRef Exp = 461 static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, 473 static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, 475 const llvm::SMTExprRef &Exp, 503 static inline llvm::SMTExprRef 510 llvm::SMTExprRef FromExp = 515 llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); 525 llvm::SMTExprRef ToExp = 530 llvm::SMTExprRef LHS = 533 llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, 568 ASTContext &Ctx, llvm::SMTExprRef &LHS, 569 llvm::SMTExprRef &RHS, QualType <y, 577 SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>( 583 SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(tools/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
2834 llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(