#include <ai.h>

Inheritance diagram for ait< domainT >:

Collaboration diagram for ait< domainT >:

Public Types
typedef goto_programt::const_targett	locationt

Public Types inherited from ai_baset
typedef ai_domain_baset	statet

typedef goto_programt::const_targett	locationt

Public Member Functions
	ait ()

domainT &	operator[] (locationt l)

const domainT &	operator[] (locationt l) const

std::unique_ptr< statet >	abstract_state_before (locationt t) const override
	Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc. More...

void	clear () override
	Resets the domain. More...

Public Member Functions inherited from ai_baset
	ai_baset ()

virtual	~ai_baset ()

void	operator() (const goto_programt &goto_program, const namespacet &ns)
	Running the interpreter. More...

void	operator() (const goto_functionst &goto_functions, const namespacet &ns)

void	operator() (const goto_modelt &goto_model)

void	operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns)

virtual std::unique_ptr< statet >	abstract_state_after (locationt l) const
	Returns the abstract state after the given instruction. More...

virtual void	output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const

void	output (const goto_modelt &goto_model, std::ostream &out) const

void	output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const

void	output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const

virtual jsont	output_json (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the domains for the whole program as JSON. More...

jsont	output_json (const goto_modelt &goto_model) const

jsont	output_json (const namespacet &ns, const goto_programt &goto_program) const

jsont	output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const

virtual xmlt	output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the domains for the whole program as XML. More...

xmlt	output_xml (const goto_modelt &goto_model) const

xmlt	output_xml (const namespacet &ns, const goto_programt &goto_program) const

xmlt	output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const

Protected Types
typedef std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt >	state_mapt

Protected Types inherited from ai_baset
typedef std::map< unsigned, locationt >	working_sett

Protected Member Functions
virtual statet &	get_state (locationt l) override

const statet &	find_state (locationt l) const override

bool	merge (const statet &src, locationt from, locationt to) override

std::unique_ptr< statet >	make_temporary_state (const statet &s) override

void	fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override

Protected Member Functions inherited from ai_baset
virtual void	initialize (const goto_programt &)

virtual void	initialize (const goto_functionst::goto_functiont &)

virtual void	initialize (const goto_functionst &)

virtual void	finalize ()

void	entry_state (const goto_programt &)

void	entry_state (const goto_functionst &)

virtual void	output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const

virtual jsont	output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
	Output the domains for a single function as JSON. More...

virtual xmlt	output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
	Output the domains for a single function as XML. More...

locationt	get_next (working_sett &working_set)

void	put_in_working_set (working_sett &working_set, locationt l)

bool	fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

void	sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)

void	concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)

bool	visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

bool	do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)

bool	do_function_call (locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)

Protected Attributes
state_mapt	state_map

Private Member Functions
void	dummy (const domainT &s)

bool	merge_shared (const statet &, goto_programt::const_targett, goto_programt::const_targett, const namespacet &) override

Detailed Description

template<typename domainT>
class ait< domainT >

Definition at line 294 of file ai.h.

Member Typedef Documentation

◆ locationt

template<typename domainT>

typedef goto_programt::const_targett ait< domainT >::locationt

Definition at line 302 of file ai.h.

◆ state_mapt

template<typename domainT>

typedef std:: unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt> ait< domainT >::state_mapt

protected

Definition at line 344 of file ai.h.

Constructor & Destructor Documentation

◆ ait()

template<typename domainT>

ait< domainT >::ait ( )

inline

Definition at line 298 of file ai.h.

Member Function Documentation

◆ abstract_state_before()

template<typename domainT>

std::unique_ptr<statet> ait< domainT >::abstract_state_before ( locationt l ) const

inlineoverridevirtual

Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc.

Intended for users of the abstract interpreter; don't use internally. Returns the abstract state before the given instruction PRECONDITION(l is dereferenceable)

Implements ai_baset.

Definition at line 322 of file ai.h.

◆ clear()

template<typename domainT>

void ait< domainT >::clear ( )

inlineoverridevirtual

Resets the domain.

Reimplemented from ai_baset.

Definition at line 335 of file ai.h.

◆ dummy()

template<typename domainT>

void ait< domainT >::dummy ( const domainT & s )

inlineprivate

Definition at line 384 of file ai.h.

◆ find_state()

template<typename domainT>

const statet& ait< domainT >::find_state ( locationt l ) const

inlineoverrideprotectedvirtual

Implements ai_baset.

Definition at line 354 of file ai.h.

◆ fixedpoint()

template<typename domainT>

void ait< domainT >::fixedpoint	(	const goto_functionst &	goto_functions,
		const namespacet &	ns
	)

inlineoverrideprotectedvirtual

Implements ai_baset.

Reimplemented in concurrency_aware_ait< domainT >, and concurrency_aware_ait< rd_range_domaint >.

Definition at line 375 of file ai.h.

◆ get_state()

template<typename domainT>

virtual statet& ait< domainT >::get_state ( locationt l )

inlineoverrideprotectedvirtual

Implements ai_baset.

Reimplemented in dependence_grapht, and reaching_definitions_analysist.

Definition at line 348 of file ai.h.

Referenced by reaching_definitions_analysist::get_state(), ait< dep_graph_domaint >::merge(), and concurrency_aware_ait< rd_range_domaint >::merge_shared().

◆ make_temporary_state()

template<typename domainT>

std::unique_ptr<statet> ait< domainT >::make_temporary_state ( const statet & s )

inlineoverrideprotectedvirtual

Implements ai_baset.

Definition at line 370 of file ai.h.

◆ merge()

template<typename domainT>

bool ait< domainT >::merge	(	const statet &	src,
		locationt	from,
		locationt	to
	)

inlineoverrideprotectedvirtual

Implements ai_baset.

Definition at line 363 of file ai.h.

Referenced by ait< dep_graph_domaint >::merge().

◆ merge_shared()

template<typename domainT>

bool ait< domainT >::merge_shared	(	const statet &	,
		goto_programt::const_targett	,
		goto_programt::const_targett	,
		const namespacet &
	)

inlineoverrideprivatevirtual

Implements ai_baset.

Reimplemented in concurrency_aware_ait< domainT >, and concurrency_aware_ait< rd_range_domaint >.

Definition at line 387 of file ai.h.

◆ operator[]() [1/2]

template<typename domainT>

domainT& ait< domainT >::operator[] ( locationt l )

inline

Definition at line 304 of file ai.h.

◆ operator[]() [2/2]

template<typename domainT>

const domainT& ait< domainT >::operator[] ( locationt l ) const

inline

Definition at line 313 of file ai.h.

Member Data Documentation

◆ state_map

template<typename domainT>

state_mapt ait< domainT >::state_map

protected

Definition at line 345 of file ai.h.

Referenced by ait< dep_graph_domaint >::abstract_state_before(), ait< dep_graph_domaint >::clear(), ait< dep_graph_domaint >::find_state(), ait< dep_graph_domaint >::get_state(), and ait< dep_graph_domaint >::operator[]().

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

analyses/ai.h

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Detailed Description

template<typename domainT> class ait< domainT >

Member Typedef Documentation

◆ locationt

◆ state_mapt

Constructor & Destructor Documentation

◆ ait()

Member Function Documentation

◆ abstract_state_before()

◆ clear()

◆ dummy()

◆ find_state()

◆ fixedpoint()

◆ get_state()

◆ make_temporary_state()

◆ merge()

◆ merge_shared()

◆ operator[]() [1/2]

◆ operator[]() [2/2]

Member Data Documentation

◆ state_map

template<typename domainT>
class ait< domainT >