#include <value_set_analysis_fivr.h>

Inheritance diagram for value_set_analysis_fivrt:

Collaboration diagram for value_set_analysis_fivrt:

Public Types
enum	track_optionst { TRACK_ALL_POINTERS, TRACK_FUNCTION_POINTERS }

typedef flow_insensitive_analysist< value_set_domain_fivrt >	baset

Public Types inherited from value_setst
typedef std::list< exprt >	valuest

Public Types inherited from flow_insensitive_analysist< value_set_domain_fivrt >
typedef goto_programt::const_targett	locationt

Public Types inherited from flow_insensitive_analysis_baset
typedef flow_insensitive_abstract_domain_baset	statet

typedef goto_programt::const_targett	locationt

Public Member Functions
	value_set_analysis_fivrt (const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)

virtual void	initialize (const goto_programt &goto_program)

virtual void	initialize (const goto_functionst &goto_functions)

void	output (locationt l, std::ostream &out)

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

virtual void	get_values (locationt l, const exprt &expr, std::list< exprt > &dest)

Public Member Functions inherited from value_setst
	value_setst ()

virtual	~value_setst ()

Public Member Functions inherited from flow_insensitive_analysist< value_set_domain_fivrt >
	flow_insensitive_analysist (const namespacet &_ns)

virtual void	clear ()

value_set_domain_fivrt &	get_data ()

const value_set_domain_fivrt &	get_data () const

Public Member Functions inherited from flow_insensitive_analysis_baset
bool	seen (const locationt &l)

	flow_insensitive_analysis_baset (const namespacet &_ns)

virtual void	update (const goto_programt &goto_program)

virtual void	update (const goto_functionst &goto_functions)

virtual void	operator() (const goto_programt &goto_program)

virtual void	operator() (const goto_functionst &goto_functions)

virtual	~flow_insensitive_analysis_baset ()

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

Protected Member Functions
bool	check_type (const typet &type)

void	get_globals (std::list< value_set_fivrt::entryt > &dest)

void	add_vars (const goto_functionst &goto_functions)

void	add_vars (const goto_programt &goto_programa)

void	get_entries (const symbolt &symbol, std::list< value_set_fivrt::entryt > &dest)

void	get_entries_rec (const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrt::entryt > &dest)

Protected Member Functions inherited from flow_insensitive_analysist< value_set_domain_fivrt >
virtual statet &	get_state ()

virtual const statet &	get_state () const

void	get_reference_set (const exprt &expr, expr_sett &expr_set)

Protected Member Functions inherited from flow_insensitive_analysis_baset
virtual void	output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const

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)

bool	fixedpoint (goto_functionst::function_mapt::const_iterator it, const goto_functionst &goto_functions)

void	fixedpoint (const goto_functionst &goto_functions)

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

bool	do_function_call_rec (locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)

bool	do_function_call (locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)

Protected Attributes
track_optionst	track_options

Protected Attributes inherited from flow_insensitive_analysist< value_set_domain_fivrt >
value_set_domain_fivrt	state

Protected Attributes inherited from flow_insensitive_analysis_baset
const namespacet &	ns

functions_donet	functions_done

recursion_sett	recursion_set

bool	initialized

Additional Inherited Members
Public Attributes inherited from flow_insensitive_analysis_baset
std::set< locationt >	seen_locations

std::map< locationt, unsigned >	statistics

Protected Types inherited from flow_insensitive_analysis_baset
typedef std::priority_queue< locationt >	working_sett

typedef std::set< irep_idt >	functions_donet

typedef std::set< irep_idt >	recursion_sett

typedef flow_insensitive_abstract_domain_baset::expr_sett	expr_sett

Static Protected Member Functions inherited from flow_insensitive_analysis_baset
static locationt	successor (locationt l)

Detailed Description

Definition at line 20 of file value_set_analysis_fivr.h.

Member Typedef Documentation

◆ baset

typedef flow_insensitive_analysist<value_set_domain_fivrt> value_set_analysis_fivrt::baset

Definition at line 36 of file value_set_analysis_fivr.h.

Member Enumeration Documentation

◆ track_optionst

enum value_set_analysis_fivrt::track_optionst

Enumerator
TRACK_ALL_POINTERS
TRACK_FUNCTION_POINTERS

Definition at line 25 of file value_set_analysis_fivr.h.

Constructor & Destructor Documentation

◆ value_set_analysis_fivrt()

value_set_analysis_fivrt::value_set_analysis_fivrt	(	const namespacet &	_ns,
		track_optionst	_track_options = `TRACK_ALL_POINTERS`
	)

inline

Definition at line 28 of file value_set_analysis_fivr.h.

Member Function Documentation

◆ add_vars() [1/2]

void value_set_analysis_fivrt::add_vars ( const goto_functionst & goto_functions )

protected

Definition at line 118 of file value_set_analysis_fivr.cpp.

References value_set_fivrt::add_vars(), forall_goto_functions, get_entries(), get_globals(), get_local_identifiers(), namespacet::lookup(), flow_insensitive_analysis_baset::ns, flow_insensitive_analysist< value_set_domain_fivrt >::state, and value_set_domain_fivrt::value_set.

Referenced by initialize().

◆ add_vars() [2/2]

void value_set_analysis_fivrt::add_vars ( const goto_programt & goto_programa )

protected

Definition at line 36 of file value_set_analysis_fivr.cpp.

References value_set_fivrt::add_vars(), goto_programt::get_decl_identifiers(), get_entries(), get_globals(), namespacet::lookup(), flow_insensitive_analysis_baset::ns, flow_insensitive_analysist< value_set_domain_fivrt >::state, and value_set_domain_fivrt::value_set.

◆ check_type()

bool value_set_analysis_fivrt::check_type ( const typet & type )

protected

Definition at line 155 of file value_set_analysis_fivr.cpp.

References struct_union_typet::components(), namespace_baset::follow(), irept::id(), flow_insensitive_analysis_baset::ns, typet::subtype(), to_struct_type(), TRACK_ALL_POINTERS, TRACK_FUNCTION_POINTERS, and track_options.

Referenced by get_entries_rec().

◆ get_entries()

void value_set_analysis_fivrt::get_entries	(	const symbolt &	symbol,
		std::list< value_set_fivrt::entryt > &	dest
	)

protected

Definition at line 74 of file value_set_analysis_fivr.cpp.

References get_entries_rec(), symbolt::name, and symbolt::type.

Referenced by add_vars(), and get_globals().

◆ get_entries_rec()

void value_set_analysis_fivrt::get_entries_rec	(	const irep_idt &	identifier,
		const std::string &	suffix,
		const typet &	type,
		std::list< value_set_fivrt::entryt > &	dest
	)