#include <ConstraintManager.h>
Public Types | |
| typedef std::pair < ProgramStateRef, ProgramStateRef > | ProgramStatePair |
Public Member Functions | |
| ConstraintManager () | |
| virtual | ~ConstraintManager () |
| virtual ProgramStateRef | assume (ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0 |
| ProgramStatePair | assumeDual (ProgramStateRef State, DefinedSVal Cond) |
| 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 ProgramStateRef | removeDeadBindings (ProgramStateRef state, SymbolReaper &SymReaper)=0 |
| virtual void | print (ProgramStateRef state, raw_ostream &Out, const char *nl, const char *sep)=0 |
| virtual void | EndPath (ProgramStateRef state) |
| ConditionTruthVal | isNull (ProgramStateRef State, SymbolRef Sym) |
Protected Member Functions | |
| virtual bool | canReasonAbout (SVal X) const =0 |
| virtual ConditionTruthVal | checkNull (ProgramStateRef State, SymbolRef Sym) |
Protected Attributes | |
| bool | NotifyAssumeClients |
Detailed Description
Definition at line 62 of file ConstraintManager.h.
Member Typedef Documentation
| typedef std::pair<ProgramStateRef, ProgramStateRef> clang::ento::ConstraintManager::ProgramStatePair |
Definition at line 71 of file ConstraintManager.h.
Constructor & Destructor Documentation
| clang::ento::ConstraintManager::ConstraintManager | ( | ) | [inline] |
Definition at line 64 of file ConstraintManager.h.
| ConstraintManager::~ConstraintManager | ( | ) | [virtual] |
Definition at line 19 of file ConstraintManager.cpp.
Member Function Documentation
| virtual ProgramStateRef clang::ento::ConstraintManager::assume | ( | ProgramStateRef | state, |
| DefinedSVal | Cond, | ||
| bool | Assumption | ||
| ) | [pure virtual] |
Implemented in clang::ento::SimpleConstraintManager.
Referenced by assumeDual(), and clang::ento::ProgramState::assumeInBound().
| ProgramStatePair clang::ento::ConstraintManager::assumeDual | ( | ProgramStateRef | State, |
| DefinedSVal | Cond | ||
| ) | [inline] |
Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false, respectively.
Definition at line 75 of file ConstraintManager.h.
References assume().
Referenced by checkNull().
| virtual bool clang::ento::ConstraintManager::canReasonAbout | ( | SVal | X | ) | const [protected, pure virtual] |
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.
Implemented in clang::ento::SimpleConstraintManager.
| ConditionTruthVal ConstraintManager::checkNull | ( | ProgramStateRef | State, |
| SymbolRef | Sym | ||
| ) | [protected, virtual] |
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"), or may be either ("underconstrained").
Definition at line 28 of file ConstraintManager.cpp.
References assumeDual(), getLocFromSymbol(), clang::ento::SymExpr::getType(), clang::ento::Loc::isLocType(), and P.
Referenced by isNull().
| virtual void clang::ento::ConstraintManager::EndPath | ( | ProgramStateRef | state | ) | [inline, virtual] |
Definition at line 120 of file ConstraintManager.h.
| virtual const llvm::APSInt* clang::ento::ConstraintManager::getSymVal | ( | ProgramStateRef | state, |
| SymbolRef | sym | ||
| ) | const [inline, virtual] |
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.
Definition at line 107 of file ConstraintManager.h.
Referenced by clang::ento::ProgramState::getSVal().
| ConditionTruthVal clang::ento::ConstraintManager::isNull | ( | ProgramStateRef | State, |
| SymbolRef | Sym | ||
| ) | [inline] |
Convenience method to query the state to see if a symbol is null or not null, or if neither assumption can be made.
Definition at line 124 of file ConstraintManager.h.
References checkNull(), and NotifyAssumeClients.
Referenced by didPreviousFreeFail(), and isLeaked().
| virtual void clang::ento::ConstraintManager::print | ( | ProgramStateRef | state, |
| raw_ostream & | Out, | ||
| const char * | nl, | ||
| const char * | sep | ||
| ) | [pure virtual] |
Referenced by clang::ento::ProgramState::print().
| virtual ProgramStateRef clang::ento::ConstraintManager::removeDeadBindings | ( | ProgramStateRef | state, |
| SymbolReaper & | SymReaper | ||
| ) | [pure virtual] |
Referenced by clang::ento::ExprEngine::removeDead().
Member Data Documentation
A flag to indicate that clients should be notified of assumptions. By default this is the case, but sometimes this needs to be restricted to avoid infinite recursions within the ConstraintManager.
Note that this flag allows the ConstraintManager to be re-entrant, but not thread-safe.
Definition at line 137 of file ConstraintManager.h.
Referenced by clang::ento::SimpleConstraintManager::assume(), and isNull().
The documentation for this class was generated from the following files: