ai_domain_baset Class Reference

The interface offered by a domain, allows code to manipulate domains without knowing their exact type. More...

#include <ai_domain.h>

Inheritance diagram for ai_domain_baset:

Public Member Functions
virtual	~ai_domain_baset ()
virtual void	transform (goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns)=0
	how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)
virtual void	output (std::ostream &out) const =0
virtual void	make_bottom ()=0
	no states
virtual void	make_top ()=0
	all states – the analysis doesn't use this, and domains may refuse to implement it.
virtual void	make_entry ()=0
	a reasonable entry-point state
virtual bool	is_bottom () const =0
virtual bool	is_top () const =0
virtual bool	ai_simplify (expr2tc &condition, const namespacet &ns) const =0
	also add
virtual bool	ai_simplify_lhs (expr2tc &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value.
virtual expr2tc	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain.

Protected Member Functions
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom'.

Detailed Description

The interface offered by a domain, allows code to manipulate domains without knowing their exact type.

Derive from this to implement domains.

Constructor & Destructor Documentation

ai_domain_baset()

ai_domain_baset::ai_domain_baset ( )

inlineprotected

The constructor is expected to produce 'false' or 'bottom'.

~ai_domain_baset()

virtual ai_domain_baset::~ai_domain_baset ( )

inlinevirtual

Member Function Documentation

ai_simplify()

virtual bool ai_domain_baset::ai_simplify ( expr2tc & condition, const namespacet & ns ) const

pure virtual

also add

bool merge(const T &b, const_targett from, const_targett to);

This computes the join between "this" and "b". Return true if "this" has changed. In the usual case, "b" is the updated state after "from" and "this" is the state before "to".

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") This method allows an expression to be simplified / evaluated using the current state. It is used to evaluate assertions and in program simplification return true if unchanged

Implemented in cse_domaint, and interval_domaint.

ai_simplify_lhs()

bool ai_domain_baset::ai_simplify_lhs ( expr2tc & condition, const namespacet & ns ) const

virtual

Simplifies the expression but keeps it as an l-value.

Use the information in the domain to simplify the expression on the LHS of an assignment.

This for example won't simplify symbols to their values, but does simplify indices in arrays, members of structs and dereferencing of pointers

Parameters

condition	the expression to simplify
ns	the namespace

Returns

True if condition did not change. False otherwise. condition will be updated with the simplified condition if it has worked

is_bottom()

virtual bool ai_domain_baset::is_bottom ( ) const

pure virtual

Implemented in cse_domaint, and interval_domaint.

is_top()

virtual bool ai_domain_baset::is_top ( ) const

pure virtual

Implemented in cse_domaint, and interval_domaint.

make_bottom()

virtual void ai_domain_baset::make_bottom ( )

pure virtual

no states

Implemented in cse_domaint, and interval_domaint.

make_entry()

virtual void ai_domain_baset::make_entry ( )

pure virtual

a reasonable entry-point state

Implemented in cse_domaint, and interval_domaint.

make_top()

virtual void ai_domain_baset::make_top ( )

pure virtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implemented in cse_domaint, and interval_domaint.

output()

virtual void ai_domain_baset::output ( std::ostream & out ) const

pure virtual

Implemented in cse_domaint, and interval_domaint.

to_predicate()

virtual expr2tc ai_domain_baset::to_predicate ( void ) const

inlinevirtual

Gives a Boolean condition that is true for all values represented by the domain.

This allows domains to be converted into program invariants.

transform()

virtual void ai_domain_baset::transform ( goto_programt::const_targett from, goto_programt::const_targett to, ai_baset & ai, const namespacet & ns )

pure virtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

Implemented in cse_domaint, and interval_domaint.

---

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

• src/goto-programs/abstract-interpretation/ai_domain.h
• src/goto-programs/abstract-interpretation/ai_domain.cpp