class SMTConv

Declaration

class SMTConv { /* full declaration omitted */ };

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:24

Method Overview

  • public static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef & Solver, const llvm::APSInt & V, clang::QualType ToTy, uint64_t ToWidth, clang::QualType FromTy, uint64_t FromWidth)
  • public template <typename T, T (*)(llvm::SMTSolverRef &, const T &, clang::QualType, uint64_t, clang::QualType, uint64_t) doCast>static inline void doFloatTypeConversion(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, T & LHS, clang::QualType & LTy, T & RHS, clang::QualType & RTy)
  • public template <typename T, T (*)(llvm::SMTSolverRef &, const T &, clang::QualType, uint64_t, clang::QualType, uint64_t) doCast>static inline void doIntTypeConversion(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, T & LHS, clang::QualType & LTy, T & RHS, clang::QualType & RTy)
  • public static inline void doTypeConversion(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, llvm::SMTExprRef & LHS, llvm::SMTExprRef & RHS, clang::QualType & LTy, clang::QualType & RTy)
  • public static inline std::pair<llvm::APSInt, QualType> fixAPSInt(clang::ASTContext & Ctx, const llvm::APSInt & Int)
  • public static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef & Solver, const llvm::SMTExprRef & LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef & RHS, bool isSigned)
  • public static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef & Solver, const llvm::SMTExprRef & Exp, clang::QualType ToTy, uint64_t ToBitWidth, clang::QualType FromTy, uint64_t FromBitWidth)
  • public static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, const clang::ento::SymbolData * Sym)
  • public static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef & Solver, const llvm::SMTExprRef & LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef & RHS)
  • public static inline llvm::SMTExprRef fromFloatSpecialBinOp(llvm::SMTSolverRef & Solver, const llvm::SMTExprRef & LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory & RHS)
  • public static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef & Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef & Exp)
  • public static inline llvm::SMTExprRef fromNBinOp(llvm::SMTSolverRef & Solver, const BinaryOperator::Opcode Op, const std::vector<llvm::SMTExprRef> & ASTs)
  • public static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef & Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef & Exp)
  • public static inline clang::QualType getAPSIntType(clang::ASTContext & Ctx, const llvm::APSInt & Int)
  • public static inline llvm::SMTExprRef getBinExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, const llvm::SMTExprRef & LHS, clang::QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef & RHS, clang::QualType RTy, clang::QualType * RetTy)
  • public static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, const llvm::SMTExprRef & Exp, clang::QualType FromTy, clang::QualType ToTy)
  • public static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, clang::ento::SymbolRef Sym, clang::QualType * RetTy = nullptr, bool * hasComparison = nullptr)
  • public static inline llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, clang::ento::SymbolRef Sym, const llvm::APSInt & From, const llvm::APSInt & To, bool InRange)
  • public static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, const clang::ento::BinarySymExpr * BSE, bool * hasComparison, clang::QualType * RetTy)
  • public static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, clang::ento::SymbolRef Sym, clang::QualType * RetTy, bool * hasComparison)
  • public static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef & Solver, clang::ASTContext & Ctx, const llvm::SMTExprRef & Exp, clang::QualType Ty, bool Assumption)
  • public static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef & Solver, const clang::QualType & Ty, unsigned int BitWidth)

Methods

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:313

Parameters

llvm::SMTSolverRef& Solver
const llvm::APSInt& V
clang::QualType ToTy
uint64_t ToWidth
clang::QualType FromTy
uint64_t FromWidth

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:753

Templates

T
T (*)(llvm::SMTSolverRef &, const T &, clang::QualType, uint64_t, clang::QualType, uint64_t) doCast

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
T& LHS
clang::QualType& LTy
T& RHS
clang::QualType& RTy

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:670

Templates

T
T (*)(llvm::SMTSolverRef &, const T &, clang::QualType, uint64_t, clang::QualType, uint64_t) doCast

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
T& LHS
clang::QualType& LTy
T& RHS
clang::QualType& RTy

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:593

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
llvm::SMTExprRef& LHS
llvm::SMTExprRef& RHS
clang::QualType& LTy
clang::QualType& RTy

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:576

Parameters

clang::ASTContext& Ctx
const llvm::APSInt& Int

static inline llvm::SMTExprRef fromBinOp(
    llvm::SMTSolverRef& Solver,
    const llvm::SMTExprRef& LHS,
    const BinaryOperator::Opcode Op,
    const llvm::SMTExprRef& RHS,
    bool isSigned)

Description

Construct an SMTSolverRef from a binary operator.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:90

Parameters

llvm::SMTSolverRef& Solver
const llvm::SMTExprRef& LHS
const BinaryOperator::Opcode Op
const llvm::SMTExprRef& RHS
bool isSigned

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

Description

Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:260

Parameters

llvm::SMTSolverRef& Solver
const llvm::SMTExprRef& Exp
clang::QualType ToTy
uint64_t ToBitWidth
clang::QualType FromTy
uint64_t FromBitWidth

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

Description

Construct an SMTSolverRef from a SymbolData.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:323

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
const clang::ento::SymbolData* Sym

static inline llvm::SMTExprRef fromFloatBinOp(
    llvm::SMTSolverRef& Solver,
    const llvm::SMTExprRef& LHS,
    const BinaryOperator::Opcode Op,
    const llvm::SMTExprRef& RHS)

Description

Construct an SMTSolverRef from a floating-point binary operator.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:201

Parameters

llvm::SMTSolverRef& Solver
const llvm::SMTExprRef& LHS
const BinaryOperator::Opcode Op
const llvm::SMTExprRef& RHS

static inline llvm::SMTExprRef
fromFloatSpecialBinOp(
    llvm::SMTSolverRef& Solver,
    const llvm::SMTExprRef& LHS,
    const BinaryOperator::Opcode Op,
    const llvm::APFloat::fltCategory& RHS)

Description

Construct an SMTSolverRef from a special floating-point binary operator.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:169

Parameters

llvm::SMTSolverRef& Solver
const llvm::SMTExprRef& LHS
const BinaryOperator::Opcode Op
const llvm::APFloat::fltCategory& RHS

static inline llvm::SMTExprRef fromFloatUnOp(
    llvm::SMTSolverRef& Solver,
    const UnaryOperator::Opcode Op,
    const llvm::SMTExprRef& Exp)

Description

Constructs an SMTSolverRef from a floating-point unary operator.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:58

Parameters

llvm::SMTSolverRef& Solver
const UnaryOperator::Opcode Op
const llvm::SMTExprRef& Exp

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

Description

Construct an SMTSolverRef from a n-ary binary operator.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:75

Parameters

llvm::SMTSolverRef& Solver
const BinaryOperator::Opcode Op
const std::vector<llvm::SMTExprRef>& ASTs

static inline llvm::SMTExprRef fromUnOp(
    llvm::SMTSolverRef& Solver,
    const UnaryOperator::Opcode Op,
    const llvm::SMTExprRef& Exp)

Description

Constructs an SMTSolverRef from an unary operator.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:39

Parameters

llvm::SMTSolverRef& Solver
const UnaryOperator::Opcode Op
const llvm::SMTExprRef& Exp

static inline clang::QualType getAPSIntType(
    clang::ASTContext& Ctx,
    const llvm::APSInt& Int)

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:569

Parameters

clang::ASTContext& Ctx
const llvm::APSInt& Int

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:346

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
const llvm::SMTExprRef& LHS
clang::QualType LTy
BinaryOperator::Opcode Op
const llvm::SMTExprRef& RHS
clang::QualType RTy
clang::QualType* RetTy

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:335

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
const llvm::SMTExprRef& Exp
clang::QualType FromTy
clang::QualType ToTy

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:487

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
clang::ento::SymbolRef Sym
clang::QualType* RetTy = nullptr
bool* hasComparison = nullptr

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:530

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
clang::ento::SymbolRef Sym
const llvm::APSInt& From
const llvm::APSInt& To
bool InRange

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:381

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
const clang::ento::BinarySymExpr* BSE
bool* hasComparison
clang::QualType* RetTy

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:422

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
clang::ento::SymbolRef Sym
clang::QualType* RetTy
bool* hasComparison

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

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:499

Parameters

llvm::SMTSolverRef& Solver
clang::ASTContext& Ctx
const llvm::SMTExprRef& Exp
clang::QualType Ty
bool Assumption

static inline llvm::SMTSortRef mkSort(
    llvm::SMTSolverRef& Solver,
    const clang::QualType& Ty,
    unsigned int BitWidth)

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:27

Parameters

llvm::SMTSolverRef& Solver
const clang::QualType& Ty
unsigned int BitWidth