#include <static_analysis.h>

Inheritance diagram for concurrency_aware_static_analysist< T >:

Collaboration diagram for concurrency_aware_static_analysist< T >:

Public Member Functions
	concurrency_aware_static_analysist (const namespacet &_ns)

virtual bool	merge_shared (static_analysis_baset::statet &a, const static_analysis_baset::statet &b, goto_programt::const_targett to)

Public Member Functions inherited from static_analysist< T >
	static_analysist (const namespacet &_ns)

T &	operator[] (locationt l)

const T &	operator[] (locationt l) const

virtual void	clear ()

virtual bool	has_location (locationt l) const

Public Member Functions inherited from static_analysis_baset
	static_analysis_baset (const namespacet &_ns)

virtual void	initialize (const goto_programt &goto_program)

virtual void	initialize (const goto_functionst &goto_functions)

virtual void	update (const goto_programt &goto_program)

virtual void	update (const goto_functionst &goto_functions)

virtual void	operator() (const irep_idt &function_identifier, const goto_programt &goto_program)

virtual void	operator() (const goto_functionst &goto_functions)

virtual	~static_analysis_baset ()

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

Protected Member Functions
virtual void	fixedpoint (const goto_functionst &goto_functions)

Protected Member Functions inherited from static_analysist< T >
virtual statet &	get_state (locationt l)

virtual const statet &	get_state (locationt l) const

virtual bool	merge (statet &a, const statet &b, locationt to)

virtual std::unique_ptr< statet >	make_temporary_state (statet &s)

virtual void	generate_state (locationt l)

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

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	get_next (working_sett &working_set)

void	put_in_working_set (working_sett &working_set, locationt l)

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

void	sequential_fixedpoint (const goto_functionst &goto_functions)

void	concurrent_fixedpoint (const goto_functionst &goto_functions)

bool	visit (const irep_idt &function_identifier, 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 (const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)

void	do_function_call (const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)

Additional Inherited Members
Public Types inherited from static_analysist< T >
typedef goto_programt::const_targett	locationt

Public Types inherited from static_analysis_baset
typedef domain_baset	statet

typedef goto_programt::const_targett	locationt

Static Public Member Functions inherited from static_analysis_baset
static exprt	get_guard (locationt from, locationt to)

static exprt	get_return_lhs (locationt to)

Protected Types inherited from static_analysist< T >
typedef std::map< locationt, T >	state_mapt

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

typedef std::set< irep_idt >	functions_donet

typedef std::set< irep_idt >	recursion_sett

typedef domain_baset::expr_sett	expr_sett

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

Protected Attributes inherited from static_analysist< T >
state_mapt	state_map

Protected Attributes inherited from static_analysis_baset
const namespacet &	ns

functions_donet	functions_done

recursion_sett	recursion_set

bool	initialized

Detailed Description

template<typename T>
class concurrency_aware_static_analysist< T >

Definition at line 384 of file static_analysis.h.

Constructor & Destructor Documentation

◆ concurrency_aware_static_analysist()

template<typename T >

concurrency_aware_static_analysist< T >::concurrency_aware_static_analysist ( const namespacet & _ns )

inlineexplicit

Definition at line 388 of file static_analysis.h.

Member Function Documentation

◆ fixedpoint()

template<typename T >

virtual void concurrency_aware_static_analysist< T >::fixedpoint ( const goto_functionst & goto_functions )

inlineprotectedvirtual

Reimplemented from static_analysist< T >.

Definition at line 405 of file static_analysis.h.

◆ merge_shared()

template<typename T >

virtual bool concurrency_aware_static_analysist< T >::merge_shared	(	static_analysis_baset::statet &	a,
		const static_analysis_baset::statet &	b,
		goto_programt::const_targett	to
	)

inlinevirtual

Reimplemented from static_analysist< T >.

Definition at line 393 of file static_analysis.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/static_analysis.h

Public Member Functions

Protected Member Functions

Additional Inherited Members

Detailed Description

template<typename T> class concurrency_aware_static_analysist< T >

Constructor & Destructor Documentation

◆ concurrency_aware_static_analysist()

Member Function Documentation

◆ fixedpoint()

◆ merge_shared()

template<typename T>
class concurrency_aware_static_analysist< T >