clang 20.0.0git
Static Public Member Functions | List of all members
clang::ento::SMTConv Class Reference

#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, QualTypefixAPSInt (ASTContext &Ctx, const llvm::APSInt &Int)
 
static void doTypeConversion (llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType &LTy, 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 &LTy, 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 &LTy, T &RHS, QualType &RTy)
 

Detailed Description

Definition at line 24 of file SMTConv.h.

Member Function Documentation

◆ castAPSInt()

static llvm::APSInt clang::ento::SMTConv::castAPSInt ( llvm::SMTSolverRef &  Solver,
const llvm::APSInt &  V,
QualType  ToTy,
uint64_t  ToWidth,
QualType  FromTy,
uint64_t  FromWidth 
)
inlinestatic

◆ doFloatTypeConversion()

template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast>
static void clang::ento::SMTConv::doFloatTypeConversion ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
T LHS,
QualType LTy,
T RHS,
QualType RTy 
)
inlinestatic

◆ doIntTypeConversion()

template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast>
static void clang::ento::SMTConv::doIntTypeConversion ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
T LHS,
QualType LTy,
T RHS,
QualType RTy 
)
inlinestatic

◆ doTypeConversion()

static void clang::ento::SMTConv::doTypeConversion ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
llvm::SMTExprRef &  LHS,
llvm::SMTExprRef &  RHS,
QualType LTy,
QualType RTy 
)
inlinestatic

◆ fixAPSInt()

static std::pair< llvm::APSInt, QualType > clang::ento::SMTConv::fixAPSInt ( ASTContext Ctx,
const llvm::APSInt &  Int 
)
inlinestatic

◆ fromBinOp()

static llvm::SMTExprRef clang::ento::SMTConv::fromBinOp ( llvm::SMTSolverRef &  Solver,
const llvm::SMTExprRef &  LHS,
const BinaryOperator::Opcode  Op,
const llvm::SMTExprRef &  RHS,
bool  isSigned 
)
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().

◆ fromCast()

static llvm::SMTExprRef clang::ento::SMTConv::fromCast ( llvm::SMTSolverRef &  Solver,
const llvm::SMTExprRef &  Exp,
QualType  ToTy,
uint64_t  ToBitWidth,
QualType  FromTy,
uint64_t  FromBitWidth 
)
inlinestatic

◆ fromData()

static llvm::SMTExprRef clang::ento::SMTConv::fromData ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
const SymbolData Sym 
)
inlinestatic

◆ fromFloatBinOp()

static llvm::SMTExprRef clang::ento::SMTConv::fromFloatBinOp ( llvm::SMTSolverRef &  Solver,
const llvm::SMTExprRef &  LHS,
const BinaryOperator::Opcode  Op,
const llvm::SMTExprRef &  RHS 
)
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().

◆ fromFloatSpecialBinOp()

static llvm::SMTExprRef clang::ento::SMTConv::fromFloatSpecialBinOp ( llvm::SMTSolverRef &  Solver,
const llvm::SMTExprRef &  LHS,
const BinaryOperator::Opcode  Op,
const llvm::APFloat::fltCategory &  RHS 
)
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().

◆ fromFloatUnOp()

static llvm::SMTExprRef clang::ento::SMTConv::fromFloatUnOp ( llvm::SMTSolverRef &  Solver,
const UnaryOperator::Opcode  Op,
const llvm::SMTExprRef &  Exp 
)
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().

◆ fromNBinOp()

static llvm::SMTExprRef clang::ento::SMTConv::fromNBinOp ( llvm::SMTSolverRef &  Solver,
const BinaryOperator::Opcode  Op,
const std::vector< llvm::SMTExprRef > &  ASTs 
)
inlinestatic

Construct an SMTSolverRef from a n-ary binary operator.

Definition at line 75 of file SMTConv.h.

◆ fromUnOp()

static llvm::SMTExprRef clang::ento::SMTConv::fromUnOp ( llvm::SMTSolverRef &  Solver,
const UnaryOperator::Opcode  Op,
const llvm::SMTExprRef &  Exp 
)
inlinestatic

Constructs an SMTSolverRef from an unary operator.

Definition at line 39 of file SMTConv.h.

Referenced by fromBinOp(), fromFloatUnOp(), getSymExpr(), and getZeroExpr().

◆ getAPSIntType()

static QualType clang::ento::SMTConv::getAPSIntType ( ASTContext Ctx,
const llvm::APSInt &  Int 
)
inlinestatic

Definition at line 571 of file SMTConv.h.

References clang::ASTContext::getIntTypeForBitwidth().

Referenced by fixAPSInt().

◆ getBinExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getBinExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
const llvm::SMTExprRef &  LHS,
QualType  LTy,
BinaryOperator::Opcode  Op,
const llvm::SMTExprRef &  RHS,
QualType  RTy,
QualType RetTy 
)
inlinestatic

◆ getCastExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getCastExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
const llvm::SMTExprRef &  Exp,
QualType  FromTy,
QualType  ToTy 
)
inlinestatic

Definition at line 335 of file SMTConv.h.

References fromCast(), and clang::ASTContext::getTypeSize().

Referenced by getSymExpr().

◆ getExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
SymbolRef  Sym,
QualType RetTy = nullptr,
bool hasComparison = nullptr 
)
inlinestatic

◆ getRangeExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getRangeExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
SymbolRef  Sym,
const llvm::APSInt &  From,
const llvm::APSInt &  To,
bool  InRange 
)
inlinestatic

◆ getSymBinExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getSymBinExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
const BinarySymExpr BSE,
bool hasComparison,
QualType RetTy 
)
inlinestatic

Definition at line 381 of file SMTConv.h.

References fixAPSInt(), getBinExpr(), clang::ento::BinarySymExpr::getOpcode(), and getSymExpr().

Referenced by getSymExpr().

◆ getSymExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getSymExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
SymbolRef  Sym,
QualType RetTy,
bool hasComparison 
)
inlinestatic

◆ getZeroExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getZeroExpr ( llvm::SMTSolverRef &  Solver,
ASTContext Ctx,
const llvm::SMTExprRef &  Exp,
QualType  Ty,
bool  Assumption 
)
inlinestatic

◆ mkSort()

static llvm::SMTSortRef clang::ento::SMTConv::mkSort ( llvm::SMTSolverRef &  Solver,
const QualType Ty,
unsigned  BitWidth 
)
inlinestatic

Definition at line 27 of file SMTConv.h.

References clang::Type::isBooleanType(), and clang::Type::isRealFloatingType().

Referenced by fromData().


The documentation for this class was generated from the following file: