clang::dataflow::Environment::BoolModel Class Reference

Abstract interface for modeling boolean formulas and path conditions in an Environment. More...

#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"

Public Member Functions
	BoolModel (BoolModelKind K)
virtual	~BoolModel ()=default
BoolModelKind	getKind () const
virtual std::unique_ptr< BoolModel >	clone () const =0
	Returns an exact copy of this model state.
virtual void	onFork ()=0
	If this model state was cloned, updates this model state to be a fork so that mutations to either model state will not affect the other.
virtual void	assume (const Formula &F)=0
	Records a fact that must be true if this point in the program is reached.
virtual bool	proves (const Formula &F) const =0
	Returns true if F is always true when this point is reached.
virtual bool	allows (const Formula &F) const =0
	Returns true if F may be true when this point is reached.
virtual BoolValue &	joinBoolValues (BoolValue &Val1, const BoolModel &Model1, BoolValue &Val2, const BoolModel &Model2, Environment &JoinedEnv)=0
	Joins two distinct boolean values Val1 (from Model1) and Val2 (from Model2) into JoinedEnv.
virtual void	join (const BoolModel &ModelA, const BoolModel &ModelB)=0
	Populates this with the join of ModelA and ModelB.
virtual LatticeEffect	widen (const BoolModel &PrevModel)=0
	Widens this with respect to PrevModel and returns whether the state changed relative to PrevModel.
virtual bool	isEquivalentTo (const BoolModel &Other) const =0
	Returns whether this boolean model state is equivalent to Other for convergence purposes.
virtual Atom	getFlowConditionToken () const =0
	Returns the flow condition token (only meaningful for SAT-based models).
virtual void	dump (raw_ostream &OS) const =0

Detailed Description

Abstract interface for modeling boolean formulas and path conditions in an Environment.

Definition at line 163 of file DataflowEnvironment.h.

Constructor & Destructor Documentation

BoolModel()

clang::dataflow::Environment::BoolModel::BoolModel ( BoolModelKind K )

inlineexplicit

Definition at line 165 of file DataflowEnvironment.h.

Referenced by isEquivalentTo(), join(), joinBoolValues(), and widen().

~BoolModel()

virtual clang::dataflow::Environment::BoolModel::~BoolModel ( )

virtualdefault

Member Function Documentation

allows()

virtual bool clang::dataflow::Environment::BoolModel::allows ( const Formula & F ) const

pure virtual

Returns true if F may be true when this point is reached.

Returns false if the formula is always false when this point is reached (or the flow condition is overly constraining). See Environment::allows for more details.

assume()

virtual void clang::dataflow::Environment::BoolModel::assume ( const Formula & F )

pure virtual

Records a fact that must be true if this point in the program is reached.

clone()

virtual std::unique_ptr< BoolModel > clang::dataflow::Environment::BoolModel::clone ( ) const

pure virtual

Returns an exact copy of this model state.

dump()

virtual void clang::dataflow::Environment::BoolModel::dump ( raw_ostream & OS ) const

pure virtual

getFlowConditionToken()

virtual Atom clang::dataflow::Environment::BoolModel::getFlowConditionToken ( ) const

pure virtual

Returns the flow condition token (only meaningful for SAT-based models).

getKind()

BoolModelKind clang::dataflow::Environment::BoolModel::getKind ( ) const

inline

Definition at line 168 of file DataflowEnvironment.h.

isEquivalentTo()

virtual bool clang::dataflow::Environment::BoolModel::isEquivalentTo ( const BoolModel & Other ) const

pure virtual

Returns whether this boolean model state is equivalent to Other for convergence purposes.

Requirements: Other must have the same kind as this.

References BoolModel(), and clang::Other.

join()

virtual void clang::dataflow::Environment::BoolModel::join ( const BoolModel & ModelA, const BoolModel & ModelB )

pure virtual

Populates this with the join of ModelA and ModelB.

Requirements: ModelA and ModelB must have the same kind as this.

References BoolModel().

joinBoolValues()

virtual BoolValue & clang::dataflow::Environment::BoolModel::joinBoolValues ( BoolValue & Val1, const BoolModel & Model1, BoolValue & Val2, const BoolModel & Model2, Environment & JoinedEnv )

pure virtual

Joins two distinct boolean values Val1 (from Model1) and Val2 (from Model2) into JoinedEnv.

Requires Model1 and Model2 to have the same kind as this.

References BoolModel(), and clang::dataflow::Environment::Environment().

onFork()

virtual void clang::dataflow::Environment::BoolModel::onFork ( )

pure virtual

If this model state was cloned, updates this model state to be a fork so that mutations to either model state will not affect the other.

proves()

virtual bool clang::dataflow::Environment::BoolModel::proves ( const Formula & F ) const

pure virtual

Returns true if F is always true when this point is reached.

Returns false if the formula may be false (or the flow condition isn't sufficiently precise to prove that it is true). See Environment::proves for more details.

widen()

virtual LatticeEffect clang::dataflow::Environment::BoolModel::widen ( const BoolModel & PrevModel )

pure virtual

Widens this with respect to PrevModel and returns whether the state changed relative to PrevModel.

Requirements: PrevModel must have the same kind as this.

References BoolModel().

---

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

• include/clang/Analysis/FlowSensitive/DataflowEnvironment.h