#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"

Inheritance diagram for clang::ento::SimpleConstraintManager:

Public Member Functions
	SimpleConstraintManager (ExprEngine *exprengine, SValBuilder &SB)
	~SimpleConstraintManager () override
Public Member Functions inherited from clang::ento::ConstraintManager
	ConstraintManager ()=default
virtual	~ConstraintManager ()
virtual bool	haveEqualConstraints (ProgramStateRef S1, ProgramStateRef S2) const =0
ProgramStateRef	assume (ProgramStateRef state, DefinedSVal Cond, bool Assumption)
ProgramStatePair	assumeDual (ProgramStateRef State, DefinedSVal Cond)
	Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false, respectively.
ProgramStateRef	assumeInclusiveRange (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)
ProgramStatePair	assumeInclusiveRangeDual (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
	Returns a pair of states (StInRange, StOutOfRange) where the given value is assumed to be in the range or out of the range, respectively.
virtual const llvm::APSInt *	getSymVal (ProgramStateRef state, SymbolRef sym) const
	If a symbol is perfectly constrained to a constant, attempt to return the concrete value.
virtual const llvm::APSInt *	getSymMinVal (ProgramStateRef state, SymbolRef sym) const
	Attempt to return the minimal possible value for a given symbol.
virtual const llvm::APSInt *	getSymMaxVal (ProgramStateRef state, SymbolRef sym) const
	Attempt to return the minimal possible value for a given symbol.
virtual ProgramStateRef	removeDeadBindings (ProgramStateRef state, SymbolReaper &SymReaper)=0
	Scan all symbols referenced by the constraints.
virtual void	printJson (raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const =0
virtual void	printValue (raw_ostream &Out, ProgramStateRef State, SymbolRef Sym)
ConditionTruthVal	isNull (ProgramStateRef State, SymbolRef Sym)
	Convenience method to query the state to see if a symbol is null or not null, or if neither assumption can be made.

Protected Member Functions
virtual ProgramStateRef	assumeSym (ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
	Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the new program state.
virtual ProgramStateRef	assumeSymInclusiveRange (ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)=0
	Given a symbolic expression within the range [From, To], assume that it is true/false and generate the new program state.
virtual ProgramStateRef	assumeSymUnsupported (ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
	Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it directly to the solver state.
ProgramStateRef	assumeInternal (ProgramStateRef State, DefinedSVal Cond, bool Assumption) override
	Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle Loc's.
ProgramStateRef	assumeInclusiveRangeInternal (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
SValBuilder &	getSValBuilder () const
BasicValueFactory &	getBasicVals () const
SymbolManager &	getSymbolManager () const
Protected Member Functions inherited from clang::ento::ConstraintManager
virtual bool	canReasonAbout (SVal X) const =0
	canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
virtual ConditionTruthVal	checkNull (ProgramStateRef State, SymbolRef Sym)
	Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"), or may be either ("underconstrained").
template<typename AssumeFunction>
ProgramStatePair	assumeDualImpl (ProgramStateRef &State, AssumeFunction &Assume)

Additional Inherited Members
Public Types inherited from clang::ento::ConstraintManager
using	ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>
Protected Attributes inherited from clang::ento::ConstraintManager
AssumeStackTy	AssumeStack

Detailed Description

Definition at line 23 of file SimpleConstraintManager.h.

Constructor & Destructor Documentation

◆ SimpleConstraintManager()

clang::ento::SimpleConstraintManager::SimpleConstraintManager	(	ExprEngine *	exprengine,
		SValBuilder &	SB )

inline

Definition at line 28 of file SimpleConstraintManager.h.

Referenced by clang::ento::RangedConstraintManager::RangedConstraintManager(), and clang::ento::SMTConstraintManager::SMTConstraintManager().

◆ ~SimpleConstraintManager()

clang::ento::SimpleConstraintManager::~SimpleConstraintManager ( )

override

Definition at line 23 of file SimpleConstraintManager.cpp.

Member Function Documentation

◆ assumeInclusiveRangeInternal()

ProgramStateRef clang::ento::SimpleConstraintManager::assumeInclusiveRangeInternal	(	ProgramStateRef	State,
		NonLoc	Value,
		const llvm::APSInt &	From,
		const llvm::APSInt &	To,
		bool	InRange )

overrideprotectedvirtual

Implements clang::ento::ConstraintManager.

Definition at line 94 of file SimpleConstraintManager.cpp.

References assumeSymInclusiveRange(), clang::ento::ConstraintManager::canReasonAbout(), and clang::Value::getKind().

◆ assumeInternal()

ProgramStateRef clang::ento::SimpleConstraintManager::assumeInternal	(	ProgramStateRef	State,
		DefinedSVal	Cond,
		bool	Assumption )

overrideprotectedvirtual

Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle Loc's.

Implements clang::ento::ConstraintManager.

Definition at line 25 of file SimpleConstraintManager.cpp.

References clang::Cond, clang::ento::SValBuilder::getStateManager(), clang::ento::ProgramStateManager::getSValBuilder(), and clang::T.

◆ assumeSym()

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

protectedpure virtual

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

Implemented in clang::ento::RangedConstraintManager, and clang::ento::SMTConstraintManager.

◆ assumeSymInclusiveRange()

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

protectedpure virtual

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.

Implemented in clang::ento::RangedConstraintManager, and clang::ento::SMTConstraintManager.

Referenced by assumeInclusiveRangeInternal().

◆ assumeSymUnsupported()

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

protectedpure virtual

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

Implemented in clang::ento::RangedConstraintManager, and clang::ento::SMTConstraintManager.

References clang::Cond.

◆ getBasicVals()

BasicValueFactory & clang::ento::SimpleConstraintManager::getBasicVals ( ) const

inlineprotected

Definition at line 79 of file SimpleConstraintManager.h.

Referenced by clang::ento::RangedConstraintManager::assumeSym(), clang::ento::SMTConstraintManager::assumeSym(), clang::ento::RangedConstraintManager::assumeSymInclusiveRange(), clang::ento::SMTConstraintManager::assumeSymInclusiveRange(), clang::ento::RangedConstraintManager::assumeSymRel(), clang::ento::RangedConstraintManager::assumeSymUnsupported(), clang::ento::SMTConstraintManager::canReasonAbout(), clang::ento::SMTConstraintManager::checkNull(), and clang::ento::SMTConstraintManager::getSymVal().

◆ getSValBuilder()

SValBuilder & clang::ento::SimpleConstraintManager::getSValBuilder ( ) const

inlineprotected

Definition at line 78 of file SimpleConstraintManager.h.

Referenced by clang::ento::SMTConstraintManager::canReasonAbout().

◆ getSymbolManager()

SymbolManager & clang::ento::SimpleConstraintManager::getSymbolManager ( ) const

inlineprotected

Definition at line 80 of file SimpleConstraintManager.h.

Referenced by clang::ento::RangedConstraintManager::assumeSym().

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

include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

Public Member Functions

Protected Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SimpleConstraintManager()

◆ ~SimpleConstraintManager()

Member Function Documentation

◆ assumeInclusiveRangeInternal()

◆ assumeInternal()

◆ assumeSym()

◆ assumeSymInclusiveRange()

◆ assumeSymUnsupported()

◆ getBasicVals()

◆ getSValBuilder()

◆ getSymbolManager()