#include <value_set_analysis.h>

Inheritance diagram for value_set_analysist:

Public Types
typedef static_analysist< value_set_domaint >	baset
using	locationt = baset::locationt
Public Types inherited from value_setst
typedef std::list< expr2tc >	valuest
typedef goto_programt::const_targett	locationt
Public Types inherited from static_analysist< value_set_domaint >
typedef goto_programt::const_targett	locationt
Public Types inherited from static_analysis_baset
typedef abstract_domain_baset	statet
typedef goto_programt::const_targett	locationt

Public Member Functions
	value_set_analysist (const namespacet &_ns)
void	initialize (const goto_programt &goto_program) override
void	initialize (const goto_functionst &goto_functions) override
void	convert (const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const
void	get_globals (std::list< value_sett::entryt > &dest)
void	get_entries_rec (const std::string &identifier, const std::string &suffix, const typet &type, std::list< value_sett::entryt > &dest)
void	get_values (locationt locationt l, const expr2tc &expr, value_setst::valuest &dest) override
void	get_reference_set (locationt locationt l, const expr2tc &expr, value_setst::valuest &dest) override
	The objects a dereference-style l-value may refer to, as object_descriptor2ts (or a raw unknown/invalid expression when no nameable object could be determined).
bool	has_location (locationt locationt l) const override
	True iff `l` carries points-to information; consumers must abstain when it does not.
Public Member Functions inherited from value_setst
	value_setst ()=default
virtual	~value_setst ()=default
Public Member Functions inherited from static_analysist< value_set_domaint >
	static_analysist (const namespacet &_ns)
value_set_domaint &	operator[] (locationt locationt l)
const value_set_domaint &	operator[] (locationt locationt l) const
void	clear () override
Public Member Functions inherited from static_analysis_baset
	static_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	~static_analysis_baset ()=default
virtual void	output (const goto_functionst &goto_functions, std::ostream &out) const
void	output (const goto_programt &goto_program, std::ostream &out) const
void	insert (locationt locationt l)

Protected Member Functions
bool	check_type (const typet &type)
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_sett::entryt > &dest)
Protected Member Functions inherited from static_analysist< value_set_domaint >
statet &	get_state (locationt locationt l) override
const statet &	get_state (locationt locationt l) const override
bool	merge (statet &a, const statet &b, bool keepnew=false) override
statet *	make_temporary_state (statet &s) override
void	generate_state (locationt locationt l) override
void	get_reference_set (locationt locationt l, const expr2tc &expr, std::list< expr2tc > &dest) override
Protected Member Functions inherited from static_analysis_baset
virtual void	output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
locationt locationt	get_next (working_sett &working_set)
void	put_in_working_set (working_sett &working_set, locationt 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 locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
void	generate_states (const goto_functionst &goto_functions)
void	generate_states (const goto_programt &goto_program)
void	do_function_call_rec (locationt locationt l_call, const expr2tc &function, const std::vector< expr2tc > &arguments, statet &new_state, const goto_functionst &goto_functions)
void	do_function_call (locationt locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const std::vector< expr2tc > &arguments, statet &new_state)

Friends
void	convert (const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
void	convert (const goto_programt &goto_program, const value_set_analysist &value_set_analysis, xmlt &dest)

Additional Inherited Members
Protected Types inherited from static_analysist< value_set_domaint >
typedef std::map< locationt locationt, value_set_domaint >	state_mapt
Protected Types inherited from static_analysis_baset
typedef std::map< unsigned, locationt locationt >	working_sett
typedef std::set< irep_idt >	functions_donet
typedef std::set< irep_idt >	recursion_sett
Static Protected Member Functions inherited from static_analysis_baset
static locationt locationt	successor (locationt locationt l)
Protected Attributes inherited from static_analysist< value_set_domaint >
state_mapt	state_map
Protected Attributes inherited from static_analysis_baset
const namespacet &	ns
functions_donet	functions_done
recursion_sett	recursion_set
bool	initialized

Member Typedef Documentation

◆ baset

typedef static_analysist<value_set_domaint> value_set_analysist::baset

◆ locationt

using value_set_analysist::locationt = baset::locationt

Constructor & Destructor Documentation

◆ value_set_analysist()

value_set_analysist::value_set_analysist ( const namespacet & _ns )

inlineexplicit

Member Function Documentation

◆ add_vars() [1/2]

void value_set_analysist::add_vars ( const goto_functionst & goto_functions )

protected

◆ add_vars() [2/2]

void value_set_analysist::add_vars ( const goto_programt & goto_programa )

protected

◆ check_type()

bool value_set_analysist::check_type ( const typet & type )

protected

◆ convert()

void value_set_analysist::convert	(	const goto_programt &	goto_program,
		const irep_idt &	identifier,
		xmlt &	dest ) const

◆ get_entries()

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

protected

◆ get_entries_rec()

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

◆ get_globals()

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

◆ get_reference_set()

void value_set_analysist::get_reference_set	(	locationt locationt	l,
		const expr2tc &	expr,
		value_setst::valuest &	dest )

inlineoverridevirtual

The objects a dereference-style l-value may refer to, as object_descriptor2ts (or a raw unknown/invalid expression when no nameable object could be determined).

Implements value_setst.

◆ get_values()

void value_set_analysist::get_values	(	locationt locationt	l,
		const expr2tc &	expr,
		value_setst::valuest &	dest )

inlineoverridevirtual

Implements value_setst.

◆ has_location()

bool value_set_analysist::has_location ( locationt locationt l ) const

inlineoverridevirtual

True iff l carries points-to information; consumers must abstain when it does not.

Implements value_setst.

◆ initialize() [1/2]

void value_set_analysist::initialize ( const goto_functionst & goto_functions )

overridevirtual

Reimplemented from static_analysis_baset.

◆ initialize() [2/2]

void value_set_analysist::initialize ( const goto_programt & goto_program )

overridevirtual

Reimplemented from static_analysis_baset.

◆ convert [1/2]

void convert	(	const goto_functionst &	goto_functions,
		const value_set_analysist &	value_set_analysis,
		xmlt &	dest )

friend

◆ convert [2/2]

void convert	(	const goto_programt &	goto_program,
		const value_set_analysist &	value_set_analysis,
		xmlt &	dest )

friend

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

src/pointer-analysis/value_set_analysis.h
src/pointer-analysis/value_set_analysis.cpp

Public Types

Public Member Functions

Protected Member Functions

Friends

Additional Inherited Members

Member Typedef Documentation

◆ baset

◆ locationt

Constructor & Destructor Documentation

◆ value_set_analysist()

Member Function Documentation

◆ add_vars() [1/2]

◆ add_vars() [2/2]

◆ check_type()

◆ convert()

◆ get_entries()

◆ get_entries_rec()

◆ get_globals()

◆ get_reference_set()

◆ get_values()

◆ has_location()

◆ initialize() [1/2]

◆ initialize() [2/2]

Friends And Related Symbol Documentation

◆ convert [1/2]

◆ convert [2/2]