#include <value_set_analysis_fi.h>

Inheritance diagram for value_set_analysis_fit:

Collaboration diagram for value_set_analysis_fit:

Public Types
enum	track_optionst { TRACK_ALL_POINTERS , TRACK_FUNCTION_POINTERS }

typedef flow_insensitive_analysist< value_set_domain_fit >	baset

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

Public Types inherited from flow_insensitive_analysist< value_set_domain_fit >
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_fit (const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)

void	initialize (const goto_programt &goto_program) override

void	initialize (const goto_functionst &goto_functions) override

std::vector< exprt >	get_values (const irep_idt &function_id, locationt l, const exprt &expr) override

Public Member Functions inherited from value_setst
	value_setst ()

virtual	~value_setst ()

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

virtual void	clear ()

value_set_domain_fit &	get_data ()

const value_set_domain_fit &	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 irep_idt &function_id, 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)

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

Protected Member Functions
bool	check_type (const typet &type)

void	get_globals (std::list< value_set_fit::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_fit::entryt > &dest)

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

Protected Member Functions inherited from flow_insensitive_analysist< value_set_domain_fit >
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
locationt	get_next (working_sett &working_set)

void	put_in_working_set (working_sett &working_set, locationt l)

bool	fixedpoint (const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)

void	fixedpoint (const goto_functionst &goto_functions)

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

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

bool	do_function_call (const irep_idt &calling_function, 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_fit >
value_set_domain_fit	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, goto_programt::target_less_than >	seen_locations

std::map< locationt, unsigned, goto_programt::target_less_than >	statistics

Protected Types inherited from flow_insensitive_analysis_baset
typedef std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_than >	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 22 of file value_set_analysis_fi.h.

Member Typedef Documentation

◆ baset

typedef flow_insensitive_analysist<value_set_domain_fit> value_set_analysis_fit::baset

Definition at line 38 of file value_set_analysis_fi.h.

Member Enumeration Documentation

◆ track_optionst

enum value_set_analysis_fit::track_optionst

Enumerator
TRACK_ALL_POINTERS
TRACK_FUNCTION_POINTERS

Definition at line 27 of file value_set_analysis_fi.h.

Constructor & Destructor Documentation

◆ value_set_analysis_fit()

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

inline

Definition at line 30 of file value_set_analysis_fi.h.

Member Function Documentation

◆ add_vars() [1/2]

void value_set_analysis_fit::add_vars ( const goto_functionst & goto_functions )

protected

Definition at line 116 of file value_set_analysis_fi.cpp.

◆ add_vars() [2/2]

void value_set_analysis_fit::add_vars ( const goto_programt & goto_programa )

protected

Definition at line 33 of file value_set_analysis_fi.cpp.

◆ check_type()

bool value_set_analysis_fit::check_type ( const typet & type )

protected

Definition at line 156 of file value_set_analysis_fi.cpp.

◆ get_entries()

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

protected

Definition at line 81 of file value_set_analysis_fi.cpp.

◆ get_entries_rec()

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

protected

Definition at line 88 of file value_set_analysis_fi.cpp.

◆ get_globals()

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

protected

Definition at line 143 of file value_set_analysis_fi.cpp.

◆ get_values()

std::vector< exprt > value_set_analysis_fit::get_values	(	const irep_idt &	function_id,
		flow_insensitive_analysis_baset::locationt	l,
		const exprt &	expr
	)

overridevirtual

Implements value_setst.

Definition at line 198 of file value_set_analysis_fi.cpp.

◆ initialize() [1/2]

void value_set_analysis_fit::initialize ( const goto_functionst & goto_functions )

overridevirtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 26 of file value_set_analysis_fi.cpp.

◆ initialize() [2/2]

void value_set_analysis_fit::initialize ( const goto_programt & goto_program )

overridevirtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 19 of file value_set_analysis_fi.cpp.

Member Data Documentation

◆ track_options

track_optionst value_set_analysis_fit::track_options

protected

Definition at line 44 of file value_set_analysis_fi.h.

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

/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_analysis_fi.h
/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_analysis_fi.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ baset

Member Enumeration Documentation

◆ track_optionst

Constructor & Destructor Documentation

◆ value_set_analysis_fit()

Member Function Documentation

◆ add_vars() [1/2]

◆ add_vars() [2/2]

◆ check_type()

◆ get_entries()

◆ get_entries_rec()

◆ get_globals()

◆ get_values()

◆ initialize() [1/2]

◆ initialize() [2/2]

Member Data Documentation

◆ track_options