#include <ai.h>

Inheritance diagram for ait< domainT >:

Public Types
typedef std::unordered_map< goto_programt::const_targett, domainT, const_target_hash, pointee_address_equalt >	state_mapt
Public Types inherited from ai_baset
typedef ai_domain_baset	statet

Public Member Functions
	ait ()
domainT &	operator[] (goto_programt::const_targett l)
bool	target_is_mapped (goto_programt::const_targett l) const
const domainT &	operator[] (goto_programt::const_targett l) const
std::unique_ptr< statet >	abstract_state_before (goto_programt::const_targett t) const override
void	clear () override
	Resets the domain.
Public Member Functions inherited from ai_baset
	ai_baset ()=default
void	operator() (const goto_programt &goto_program, const namespacet &ns)
	Run analysis over Program.
void	operator() (const goto_functionst &goto_functions, const namespacet &ns)
	Run analysis over Module (Goto Functions).
virtual std::unique_ptr< statet >	abstract_state_after (goto_programt::const_targett l) const
virtual void	output (const goto_functionst &goto_functions, std::ostream &out) const

Public Attributes
state_mapt	state_map
Public Attributes inherited from ai_baset
bool	continue_past_failed_assertions = false
	goto_programt::get_successors gives an ASSERT whose guard is false no successor, as though a violation ended the run.

Protected Member Functions
virtual statet &	get_state (goto_programt::const_targett l) override
const statet &	find_state (goto_programt::const_targett l) const override
bool	merge (const statet &src, goto_programt::const_targett from, goto_programt::const_targett 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_functiont &)
virtual void	initialize (const goto_functionst &)
virtual void	finalize ()
void	entry_state (const goto_programt &)
void	entry_state (const goto_functionst &)
goto_programt::const_targett	get_next (working_sett &working_set)
void	put_in_working_set (working_sett &working_set, goto_programt::const_targett 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)
bool	visit (goto_programt::const_targett l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
bool	do_function_call_rec (goto_programt::const_targett l_call, goto_programt::const_targett l_return, const expr2tc &function, const goto_functionst &goto_functions, const namespacet &ns)
bool	do_function_call (goto_programt::const_targett l_call, goto_programt::const_targett l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const namespacet &ns)

Additional Inherited Members
Protected Types inherited from ai_baset
typedef std::unordered_map< unsigned, goto_programt::const_targett >	working_sett

Member Typedef Documentation

◆ state_mapt

template<typename domainT>

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

Constructor & Destructor Documentation

◆ ait()

template<typename domainT>

ait< domainT >::ait ( )

inline

Member Function Documentation

◆ abstract_state_before()

template<typename domainT>

std::unique_ptr< statet > ait< domainT >::abstract_state_before ( goto_programt::const_targett t ) const

inlineoverridevirtual

Implements ai_baset.

◆ clear()

template<typename domainT>

void ait< domainT >::clear ( )

inlineoverridevirtual

Resets the domain.

Reimplemented from ai_baset.