reference, declarationdefinition
definition → references, declarations, derived classes, virtual overrides
reference to multiple definitions → definitions
unreferenced

References

include/llvm/Support/SMTAPI.h
  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 &LTy,
  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(