#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, message_handlert &)

virtual	~reaching_definitions_analysist ()

void	initialize (const goto_functionst &goto_functions) override
	Initialize all the abstract states for a whole program. More...

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

	concurrency_aware_ait (std::unique_ptr< ai_domain_factory_baset > &&df)

virtual bool	merge_shared (const statet &src, locationt from, locationt to, const namespacet &ns)

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

	ait (std::unique_ptr< ai_domain_factory_baset > &&df)

const domainT &	operator[] (locationt l) const
	Find the analysis result for a given location. More...

Public Member Functions inherited from ai_recursive_interproceduralt
	ai_recursive_interproceduralt (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)

Public Member Functions inherited from ai_baset
	ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)

virtual	~ai_baset ()

void	operator() (const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
	Run abstract interpretation on a single function. More...

void	operator() (const goto_functionst &goto_functions, const namespacet &ns)
	Run abstract interpretation on a whole program. More...

void	operator() (const abstract_goto_modelt &goto_model)
	Run abstract interpretation on a whole program. More...

void	operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
	Run abstract interpretation on a single function. More...

virtual ctrace_set_ptrt	abstract_traces_before (locationt l) const
	Returns all of the histories that have reached the start of the instruction. More...

virtual ctrace_set_ptrt	abstract_traces_after (locationt l) const
	Returns all of the histories that have reached the end of the instruction. More...

virtual cstate_ptrt	abstract_state_before (locationt l) const
	Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...

virtual cstate_ptrt	abstract_state_after (locationt l) const
	Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used. More...

virtual cstate_ptrt	abstract_state_before (const trace_ptrt &p) const
	The same interfaces but with histories. More...

virtual cstate_ptrt	abstract_state_after (const trace_ptrt &p) const

virtual void	clear ()
	Reset the abstract state. More...

virtual void	output (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
	Output the abstract states for a single function. More...

virtual jsont	output_json (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
	Output the abstract states for a single function as JSON. More...

virtual xmlt	output_xml (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
	Output the abstract states for a single function as XML. More...

virtual void	output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
	Output the abstract states for a whole program. More...

void	output (const goto_modelt &goto_model, std::ostream &out) const
	Output the abstract states for a whole program. More...

void	output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
	Output the abstract states for a function. More...

virtual jsont	output_json (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the abstract states for the whole program as JSON. More...

jsont	output_json (const goto_modelt &goto_model) const
	Output the abstract states for a whole program as JSON. More...

jsont	output_json (const namespacet &ns, const goto_programt &goto_program) const
	Output the abstract states for a single function as JSON. More...

jsont	output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
	Output the abstract states for a single function as JSON. More...

virtual xmlt	output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the abstract states for the whole program as XML. More...

xmlt	output_xml (const goto_modelt &goto_model) const
	Output the abstract states for the whole program as XML. More...

xmlt	output_xml (const namespacet &ns, const goto_programt &goto_program) const
	Output the abstract states for a single function as XML. More...

xmlt	output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
	Output the abstract states for a single function as XML. More...

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

std::unique_ptr< value_setst >	value_sets

std::unique_ptr< is_threadedt >	is_threaded

std::unique_ptr< dirtyt >	is_dirty

Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_baset >	history_factory
	For creating history objects. More...

std::unique_ptr< ai_domain_factory_baset >	domain_factory
	For creating domain objects. More...

std::unique_ptr< ai_storage_baset >	storage

message_handlert &	message_handler

Protected Attributes inherited from sparse_bitvector_analysist< reaching_definitiont >
std::vector< typename inner_mapt::const_iterator >	values
	It is a map from an `ID` to the corresponding `reaching_definitiont` instance inside the map `value_map`. More...

std::unordered_map< irep_idt, inner_mapt >	value_map
	A map from names of program variables to a set of pairs (`reaching_definitiont`, `ID`). More...

Additional Inherited Members
Public Types inherited from concurrency_aware_ait< rd_range_domaint >
using	statet = typename ait< rd_range_domaint >::statet

using	locationt = typename statet::locationt

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

Public Types inherited from ai_baset
typedef ai_domain_baset	statet

typedef ai_storage_baset::cstate_ptrt	cstate_ptrt

typedef ai_history_baset::trace_ptrt	trace_ptrt

typedef ai_history_baset::trace_sett	trace_sett

typedef ai_storage_baset::ctrace_set_ptrt	ctrace_set_ptrt

typedef goto_programt::const_targett	locationt

Protected Types inherited from concurrency_aware_ait< rd_range_domaint >
using	working_sett = ai_baset::working_sett

Protected Types inherited from ai_baset
typedef trace_sett	working_sett
	The work queue, sorted using the history's ordering operator. More...

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 (ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override

Protected Member Functions inherited from ait< domainT >
virtual statet &	get_state (locationt l)

virtual statet &	get_state (trace_ptrt p)
	Get the state for the given history, creating it with the factory if it doesn't exist. More...

Protected Member Functions inherited from ai_recursive_interproceduralt
bool	visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override

Protected Member Functions inherited from ai_baset
virtual void	initialize (const irep_idt &function_id, const goto_programt &goto_program)
	Initialize all the abstract states for a single function. More...

virtual void	initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function)
	Initialize all the abstract states for a single function. More...

virtual void	finalize ()
	Override this to add a cleanup or post-processing step after fixedpoint has run. More...

trace_ptrt	entry_state (const goto_programt &goto_program)
	Set the abstract state of the entry location of a single function to the entry state required by the analysis. More...

trace_ptrt	entry_state (const goto_functionst &goto_functions)
	Set the abstract state of the entry location of a whole program to the entry state required by the analysis. More...

trace_ptrt	get_next (working_sett &working_set)
	Get the next location from the work queue. More...

void	put_in_working_set (working_sett &working_set, trace_ptrt t)

virtual bool	fixedpoint (trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
	Run the fixedpoint algorithm until it reaches a fixed point. More...

virtual bool	visit (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
	Perform one step of abstract interpretation from trace t Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...

virtual bool	visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

virtual bool	visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

bool	visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)

virtual bool	merge (const statet &src, trace_ptrt from, trace_ptrt to)
	Merge the state `src`, flowing from tracet `from` to tracet `to`, into the state currently stored for tracet `to`. More...

virtual std::unique_ptr< statet >	make_temporary_state (const statet &s)
	Make a copy of a state. More...

virtual statet &	get_state (trace_ptrt p)
	Get the state for the given history, creating it with the factory if it doesn't exist. More...

Detailed Description

Definition at line 349 of file reaching_definitions.h.

Constructor & Destructor Documentation

◆ reaching_definitions_analysist()

reaching_definitions_analysist::reaching_definitions_analysist	(	const namespacet &	_ns,
		message_handlert &	message_handler
	)

Definition at line 54 of file reaching_definitions.cpp.

◆ ~reaching_definitions_analysist()

reaching_definitions_analysist::~reaching_definitions_analysist ( )

virtualdefault

Member Function Documentation

◆ get_is_dirty()

const dirtyt& reaching_definitions_analysist::get_is_dirty ( ) const

inline

Definition at line 373 of file reaching_definitions.h.

◆ get_is_threaded()

const is_threadedt& reaching_definitions_analysist::get_is_threaded ( ) const

inline

Definition at line 367 of file reaching_definitions.h.

◆ get_value_sets()

value_setst& reaching_definitions_analysist::get_value_sets ( ) const

inline

Definition at line 361 of file reaching_definitions.h.

◆ initialize()

void reaching_definitions_analysist::initialize ( const goto_functionst & goto_functions )

overridevirtual

Initialize all the abstract states for a whole program.

Override this to do custom per-analysis initialization.

Reimplemented from ai_baset.

Definition at line 736 of file reaching_definitions.cpp.

Member Data Documentation

◆ is_dirty

std::unique_ptr<dirtyt> reaching_definitions_analysist::is_dirty

protected

Definition at line 383 of file reaching_definitions.h.

◆ is_threaded

std::unique_ptr<is_threadedt> reaching_definitions_analysist::is_threaded

protected

Definition at line 382 of file reaching_definitions.h.

◆ ns

const namespacet& reaching_definitions_analysist::ns

protected

Definition at line 380 of file reaching_definitions.h.

◆ value_sets

std::unique_ptr<value_setst> reaching_definitions_analysist::value_sets

protected

Definition at line 381 of file reaching_definitions.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/reaching_definitions.h
/home/runner/work/cbmc/cbmc/src/analyses/reaching_definitions.cpp

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ reaching_definitions_analysist()

◆ ~reaching_definitions_analysist()

Member Function Documentation

◆ get_is_dirty()

◆ get_is_threaded()

◆ get_value_sets()

◆ initialize()

Member Data Documentation

◆ is_dirty

◆ is_threaded

◆ ns

◆ value_sets