#include <reaching_definitions.h>

Inheritance diagram for reaching_definitions_analysist:

Collaboration diagram for reaching_definitions_analysist:

Public Member Functions
	reaching_definitions_analysist (const namespacet &_ns)

virtual	~reaching_definitions_analysist ()

virtual void	initialize (const goto_functionst &goto_functions)

virtual statet &	get_state (goto_programt::const_targett l)

value_setst &	get_value_sets () const

const is_threadedt &	get_is_threaded () const

const dirtyt &	get_is_dirty () const

Public Member Functions inherited from concurrency_aware_ait< rd_range_domaint >
	concurrency_aware_ait ()

bool	merge_shared (const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override

Public Member Functions inherited from ait< rd_range_domaint >
	ait ()

rd_range_domaint &	operator[] (locationt l)

const rd_range_domaint &	operator[] (locationt l) const

void	clear () override

Public Member Functions inherited from ai_baset
	ai_baset ()

virtual	~ai_baset ()

void	operator() (const goto_programt &goto_program, const namespacet &ns)

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 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

Public Member Functions inherited from sparse_bitvector_analysist< reaching_definitiont >
const reaching_definitiont &	get (const std::size_t value_index) const

std::size_t	add (const reaching_definitiont &value)

void	clear ()

Protected Attributes
const namespacet &	ns

value_setst *	value_sets

is_threadedt *	is_threaded

dirtyt *	is_dirty

Protected Attributes inherited from ait< rd_range_domaint >
state_mapt	state_map

Protected Attributes inherited from ai_baset
recursion_sett	recursion_set

Protected Attributes inherited from sparse_bitvector_analysist< reaching_definitiont >
std::vector< typename inner_mapt::const_iterator >	values

std::unordered_map< irep_idt, inner_mapt, irep_id_hash >	value_map

Additional Inherited Members
Public Types inherited from concurrency_aware_ait< rd_range_domaint >
typedef ait< rd_range_domaint >::statet	statet

Public Types inherited from ait< rd_range_domaint >
typedef goto_programt::const_targett	locationt

Public Types inherited from ai_baset
typedef ai_domain_baset	statet

typedef goto_programt::const_targett	locationt

Protected Types inherited from ait< rd_range_domaint >
typedef std::unordered_map< locationt, rd_range_domaint, const_target_hash >	state_mapt

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

typedef std::set< irep_idt >	recursion_sett

Protected Types inherited from sparse_bitvector_analysist< reaching_definitiont >
typedef std::map< reaching_definitiont, std::size_t >	inner_mapt

Protected Member Functions inherited from concurrency_aware_ait< rd_range_domaint >
void	fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override

Protected Member Functions inherited from ait< rd_range_domaint >
const statet &	find_state (locationt l) const override

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

statet *	make_temporary_state (const statet &s) override

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

virtual void	initialize (const goto_functionst::goto_functiont &)

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)