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

Inheritance diagram for clang::ento::SimpleConstraintManager:

[legend]

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 ProgramStateRef	assumeInternal (ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0

virtual ProgramStateRef	assumeInclusiveRangeInternal (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)=0

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.

◆ ~SimpleConstraintManager()

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

override

Definition at line 24 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 95 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 26 of file SimpleConstraintManager.cpp.

References clang::ASTContext::BoolTy, clang::ento::SVal::castAs(), clang::ento::SValBuilder::evalCast(), clang::ento::SVal::getAs(), clang::ento::SValBuilder::getContext(), clang::T, and clang::ASTContext::VoidPtrTy.

◆ 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
	)