class SMTConstraintManager

Declaration

class SMTConstraintManager : public SimpleConstraintManager { /* full declaration omitted */ };

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:30

Inherits from: SimpleConstraintManager

Member Variables

private llvm::SMTSolverRef Solver = llvm::CreateZ3Solver()

protected llvm::DenseMap<unsigned int, ConditionTruthVal> Cached

Inherited from ConstraintManager:

protected AssumeStack

Method Overview

• public SMTConstraintManager(clang::ento::ExprEngine * EE, clang::ento::SValBuilder & SB)
• protected virtual void addStateConstraints(clang::ento::ProgramStateRef State) const
• protected virtual clang::ento::ProgramStateRef assumeExpr(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym, const llvm::SMTExprRef & Exp)
• public clang::ento::ProgramStateRef assumeSym(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym, bool Assumption)
• public clang::ento::ProgramStateRef assumeSymInclusiveRange(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym, const llvm::APSInt & From, const llvm::APSInt & To, bool InRange)
• public clang::ento::ProgramStateRef assumeSymUnsupported(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym, bool Assumption)
• public bool canReasonAbout(clang::ento::SVal X) const
• protected clang::ento::ConditionTruthVal checkModel(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym, const llvm::SMTExprRef & Exp) const
• public clang::ento::ConditionTruthVal checkNull(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym)
• public void dump() const
• public const llvm::APSInt * getSymVal(clang::ento::ProgramStateRef State, clang::ento::SymbolRef Sym) const
• public bool haveEqualConstraints(clang::ento::ProgramStateRef S1, clang::ento::ProgramStateRef S2) const
• public void printJson(llvm::raw_ostream & Out, clang::ento::ProgramStateRef State, const char * NL = "\n", unsigned int Space = 0, bool IsDot = false) const
• public clang::ento::ProgramStateRef removeDeadBindings(clang::ento::ProgramStateRef State, clang::ento::SymbolReaper & SymReaper)
• public virtual ~SMTConstraintManager()

Inherited from SimpleConstraintManager:

• protected assumeInclusiveRangeInternal
• protected assumeInternal
• protected assumeSym
• protected assumeSymInclusiveRange
• protected assumeSymUnsupported
• protected getBasicVals
• protected getSValBuilder
• protected getSymbolManager

Inherited from ConstraintManager:

• public assume
• public assumeDual
• protected assumeDualImpl
• public assumeInclusiveRange
• public assumeInclusiveRangeDual
• protected assumeInclusiveRangeInternal
• protected assumeInternal
• protected canReasonAbout
• protected checkNull
• public getSymVal
• public haveEqualConstraints
• public isNull
• public printJson
• public printValue
• public removeDeadBindings

Methods

¶SMTConstraintManager(clang::ento::ExprEngine* EE,
                     clang::ento::SValBuilder& SB)

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:34

Parameters

clang::ento::ExprEngine* EE

clang::ento::SValBuilder& SB

¶virtual void addStateConstraints(
    clang::ento::ProgramStateRef State) const

Description

Given a program state, construct the logical conjunction and add it to the solver

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:308

Parameters

clang::ento::ProgramStateRef State

¶virtual clang::ento::ProgramStateRef assumeExpr(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym,
    const llvm::SMTExprRef& Exp)

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:297

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

const llvm::SMTExprRef& Exp

¶clang::ento::ProgramStateRef assumeSym(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym,
    bool Assumption)

Description

Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the new program state.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:43

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

bool Assumption

¶clang::ento::ProgramStateRef
assumeSymInclusiveRange(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym,
    const llvm::APSInt& From,
    const llvm::APSInt& To,
    bool InRange)

Description

Given a symbolic expression within the range [From, To], assume that it is true/false and generate the new program state. This function is used to handle case ranges produced by a language extension for switch case statements.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:63

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

const llvm::APSInt& From

const llvm::APSInt& To

bool InRange

¶clang::ento::ProgramStateRef assumeSymUnsupported(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym,
    bool Assumption)

Description

Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it directly to the solver state.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:72

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

bool Assumption

¶bool canReasonAbout(clang::ento::SVal X) const

Description

canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values. This method returns true if the ConstraintManager can reasonably handle a given SVal value. This is typically queried by ExprEngine to determine if the value should be replaced with a conjured symbolic value in order to recover some precision.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:246

Parameters

clang::ento::SVal X

¶clang::ento::ConditionTruthVal checkModel(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym,
    const llvm::SMTExprRef& Exp) const

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:327

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

const llvm::SMTExprRef& Exp

¶clang::ento::ConditionTruthVal checkNull(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym)

Description

Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"), or may be either ("underconstrained").

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:82

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

¶void dump() const

Description

Dumps SMT formula

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:293

¶const llvm::APSInt* getSymVal(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolRef Sym) const

Description

If a symbol is perfectly constrained to a constant, attempt to return the concrete value. Note that a ConstraintManager is not obligated to return a concretized value for a symbol, even if it is perfectly constrained. It might return null.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:110

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolRef Sym

¶bool haveEqualConstraints(
    clang::ento::ProgramStateRef S1,
    clang::ento::ProgramStateRef S2) const

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:241

Parameters

clang::ento::ProgramStateRef S1

clang::ento::ProgramStateRef S2

¶void printJson(llvm::raw_ostream& Out,
               clang::ento::ProgramStateRef State,
               const char* NL = "\n",
               unsigned int Space = 0,
               bool IsDot = false) const

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:213

Parameters

llvm::raw_ostream& Out

clang::ento::ProgramStateRef State

const char* NL = "\n"

unsigned int Space = 0

bool IsDot = false

¶clang::ento::ProgramStateRef removeDeadBindings(
    clang::ento::ProgramStateRef State,
    clang::ento::SymbolReaper& SymReaper)

Description

Scan all symbols referenced by the constraints. If the symbol is not alive, remove it.

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:200

Parameters

clang::ento::ProgramStateRef State

clang::ento::SymbolReaper& SymReaper

¶virtual ~SMTConstraintManager()

Declared at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:37