clang 20.0.0git
|
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
Static Public Member Functions | |
static llvm::SMTSortRef | mkSort (llvm::SMTSolverRef &Solver, const QualType &Ty, unsigned BitWidth) |
static llvm::SMTExprRef | fromUnOp (llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp) |
Constructs an SMTSolverRef from an unary operator. | |
static llvm::SMTExprRef | fromFloatUnOp (llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp) |
Constructs an SMTSolverRef from a floating-point unary operator. | |
static llvm::SMTExprRef | fromNBinOp (llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, const std::vector< llvm::SMTExprRef > &ASTs) |
Construct an SMTSolverRef from a n-ary binary operator. | |
static llvm::SMTExprRef | fromBinOp (llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned) |
Construct an SMTSolverRef from a binary operator. | |
static llvm::SMTExprRef | fromFloatSpecialBinOp (llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS) |
Construct an SMTSolverRef from a special floating-point binary operator. | |
static llvm::SMTExprRef | fromFloatBinOp (llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS) |
Construct an SMTSolverRef from a floating-point binary operator. | |
static llvm::SMTExprRef | fromCast (llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth) |
Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths. | |
static llvm::APSInt | castAPSInt (llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth) |
static llvm::SMTExprRef | fromData (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) |
Construct an SMTSolverRef from a SymbolData. | |
static llvm::SMTExprRef | getCastExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType FromTy, QualType ToTy) |
static llvm::SMTExprRef | getBinExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, QualType RTy, QualType *RetTy) |
static llvm::SMTExprRef | getSymBinExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy) |
static llvm::SMTExprRef | getSymExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, bool *hasComparison) |
static llvm::SMTExprRef | getExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr) |
static llvm::SMTExprRef | getZeroExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption) |
static llvm::SMTExprRef | getRangeExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) |
static QualType | getAPSIntType (ASTContext &Ctx, const llvm::APSInt &Int) |
static std::pair< llvm::APSInt, QualType > | fixAPSInt (ASTContext &Ctx, const llvm::APSInt &Int) |
static void | doTypeConversion (llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType <y, QualType &RTy) |
template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast> | |
static void | doIntTypeConversion (llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType <y, T &RHS, QualType &RTy) |
template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast> | |
static void | doFloatTypeConversion (llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType <y, T &RHS, QualType &RTy) |
|
inlinestatic |
Definition at line 313 of file SMTConv.h.
References clang::ento::APSIntType::convert(), clang::Type::isSignedIntegerOrEnumerationType(), and V.
|
inlinestatic |
Definition at line 755 of file SMTConv.h.
References clang::ASTContext::getFloatingTypeOrder(), clang::ASTContext::getTypeSize(), and clang::Type::isRealFloatingType().
|
inlinestatic |
Definition at line 672 of file SMTConv.h.
References clang::ASTContext::getCorrespondingUnsignedType(), clang::ASTContext::getIntegerTypeOrder(), clang::ASTContext::getPromotedIntegerType(), clang::ASTContext::getTypeSize(), clang::QualType::isNull(), clang::ASTContext::isPromotableIntegerType(), and clang::Type::isSignedIntegerOrEnumerationType().
|
inlinestatic |
Definition at line 595 of file SMTConv.h.
References fromCast(), clang::QualType::getCanonicalType(), clang::ASTContext::getTypeSize(), clang::Type::isAnyPointerType(), clang::Type::isArithmeticType(), clang::Type::isBlockPointerType(), clang::Type::isIntegralOrEnumerationType(), clang::QualType::isNull(), clang::Type::isNullPtrType(), clang::Type::isObjCObjectPointerType(), clang::Type::isRealFloatingType(), clang::Type::isReferenceType(), and clang::Type::isVoidPointerType().
Referenced by getBinExpr().
|
inlinestatic |
Definition at line 578 of file SMTConv.h.
References clang::ASTContext::BoolTy, getAPSIntType(), and clang::ASTContext::getTypeSize().
Referenced by getRangeExpr(), getSymBinExpr(), and clang::ento::SMTConstraintManager::getSymVal().
|
inlinestatic |
Construct an SMTSolverRef from a binary operator.
Definition at line 90 of file SMTConv.h.
References fromBinOp(), and fromUnOp().
Referenced by fromBinOp(), fromFloatBinOp(), getBinExpr(), getRangeExpr(), clang::ento::SMTConstraintManager::getSymVal(), and getZeroExpr().
|
inlinestatic |
Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths.
Definition at line 260 of file SMTConv.h.
References clang::Type::isAnyPointerType(), clang::Type::isBlockPointerType(), clang::Type::isBooleanType(), clang::Type::isIntegralOrEnumerationType(), clang::Type::isRealFloatingType(), clang::Type::isReferenceType(), and clang::Type::isSignedIntegerOrEnumerationType().
Referenced by doTypeConversion(), and getCastExpr().
|
inlinestatic |
Construct an SMTSolverRef from a SymbolData.
Definition at line 323 of file SMTConv.h.
References clang::ento::SymbolData::getKindStr(), clang::ento::SymbolData::getSymbolID(), clang::ento::SymExpr::getType(), clang::ASTContext::getTypeSize(), ID, mkSort(), and clang::ento::OS.
Referenced by getSymExpr(), and clang::ento::SMTConstraintManager::getSymVal().
|
inlinestatic |
Construct an SMTSolverRef from a floating-point binary operator.
Definition at line 201 of file SMTConv.h.
References fromBinOp(), fromFloatBinOp(), and fromFloatUnOp().
Referenced by fromFloatBinOp(), getBinExpr(), and getZeroExpr().
|
inlinestatic |
Construct an SMTSolverRef from a special floating-point binary operator.
Definition at line 169 of file SMTConv.h.
References fromFloatSpecialBinOp(), and fromFloatUnOp().
Referenced by fromFloatSpecialBinOp().
|
inlinestatic |
Constructs an SMTSolverRef from a floating-point unary operator.
Definition at line 58 of file SMTConv.h.
References fromUnOp().
Referenced by fromFloatBinOp(), fromFloatSpecialBinOp(), and getSymExpr().
|
inlinestatic |
|
inlinestatic |
Constructs an SMTSolverRef from an unary operator.
Definition at line 39 of file SMTConv.h.
Referenced by fromBinOp(), fromFloatUnOp(), getSymExpr(), and getZeroExpr().
|
inlinestatic |
Definition at line 571 of file SMTConv.h.
References clang::ASTContext::getIntTypeForBitwidth().
Referenced by fixAPSInt().
|
inlinestatic |
Definition at line 346 of file SMTConv.h.
References clang::ASTContext::BoolTy, doTypeConversion(), fromBinOp(), fromFloatBinOp(), clang::ASTContext::getPointerDiffType(), clang::Type::isAnyPointerType(), clang::BinaryOperator::isComparisonOp(), clang::BinaryOperator::isLogicalOp(), clang::Type::isRealFloatingType(), and clang::Type::isSignedIntegerOrEnumerationType().
Referenced by getRangeExpr(), and getSymBinExpr().
|
inlinestatic |
Definition at line 335 of file SMTConv.h.
References fromCast(), and clang::ASTContext::getTypeSize().
Referenced by getSymExpr().
|
inlinestatic |
Definition at line 489 of file SMTConv.h.
References getSymExpr().
Referenced by clang::ento::SMTConstraintManager::assumeSym(), clang::ento::SMTConstraintManager::checkNull(), and getRangeExpr().
|
inlinestatic |
Definition at line 532 of file SMTConv.h.
References fixAPSInt(), fromBinOp(), getBinExpr(), getExpr(), and clang::Type::isSignedIntegerOrEnumerationType().
Referenced by clang::ento::SMTConstraintManager::assumeSymInclusiveRange(), and clang::ento::Z3CrosscheckVisitor::finalizeVisitor().
|
inlinestatic |
Definition at line 381 of file SMTConv.h.
References fixAPSInt(), getBinExpr(), clang::ento::BinarySymExpr::getOpcode(), and getSymExpr().
Referenced by getSymExpr().
|
inlinestatic |
Definition at line 422 of file SMTConv.h.
References fromData(), fromFloatUnOp(), fromUnOp(), getCastExpr(), getSymBinExpr(), getSymExpr(), clang::ento::SymExpr::getType(), clang::ASTContext::getTypeSize(), clang::BinaryOperator::isComparisonOp(), and clang::Type::isRealFloatingType().
Referenced by getExpr(), getSymBinExpr(), and getSymExpr().
|
inlinestatic |
Definition at line 501 of file SMTConv.h.
References fromBinOp(), fromFloatBinOp(), fromUnOp(), clang::ASTContext::getFloatTypeSemantics(), clang::ASTContext::getTypeSize(), clang::Type::isAnyPointerType(), clang::Type::isBlockPointerType(), clang::Type::isBooleanType(), clang::Type::isIntegralOrEnumerationType(), clang::Type::isRealFloatingType(), clang::Type::isReferenceType(), and clang::Type::isSignedIntegerOrEnumerationType().
Referenced by clang::ento::SMTConstraintManager::assumeSym(), and clang::ento::SMTConstraintManager::checkNull().
|
inlinestatic |
Definition at line 27 of file SMTConv.h.
References clang::Type::isBooleanType(), and clang::Type::isRealFloatingType().
Referenced by fromData().