#include <static_analysis.h>

Inheritance diagram for static_analysist< T >:

Collaboration diagram for static_analysist< T >:

Public Types
typedef goto_programt::const_targett	locationt

Public Types inherited from static_analysis_baset
typedef domain_baset	statet

typedef goto_programt::const_targett	locationt

Public Member Functions
	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 Types
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

Protected Member Functions
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)

virtual void	fixedpoint (const goto_functionst &goto_functions)

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)

Protected Attributes
state_mapt	state_map

Protected Attributes inherited from static_analysis_baset
const namespacet &	ns

functions_donet	functions_done

recursion_sett	recursion_set

bool	initialized

Private Member Functions
void	dummy (const T &s)

virtual bool	merge_shared (statet &, const statet &, goto_programt::const_targett)

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

static exprt	get_return_lhs (locationt to)

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

Detailed Description

template<typename T>
class static_analysist< T >

Definition at line 279 of file static_analysis.h.

Member Typedef Documentation

◆ locationt

template<typename T >

typedef goto_programt::const_targett static_analysist< T >::locationt

Definition at line 288 of file static_analysis.h.

◆ state_mapt

template<typename T >

typedef std::map<locationt, T> static_analysist< T >::state_mapt

protected

Definition at line 320 of file static_analysis.h.

Constructor & Destructor Documentation

◆ static_analysist()

template<typename T >

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

inlineexplicit

Definition at line 283 of file static_analysis.h.

Member Function Documentation

◆ clear()

template<typename T >

virtual void static_analysist< T >::clear ( )

inlinevirtual

Reimplemented from static_analysis_baset.

Definition at line 308 of file static_analysis.h.

◆ dummy()

template<typename T >

void static_analysist< T >::dummy ( const T & s )

inlineprivate

Definition at line 371 of file static_analysis.h.

◆ fixedpoint()

template<typename T >

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

inlineprotectedvirtual

Implements static_analysis_baset.

Reimplemented in concurrency_aware_static_analysist< T >.

Definition at line 364 of file static_analysis.h.

◆ generate_state()

template<typename T >

virtual void static_analysist< T >::generate_state ( locationt l )

inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 351 of file static_analysis.h.

◆ get_reference_set()

template<typename T >

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

inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 356 of file static_analysis.h.

◆ get_state() [1/2]

template<typename T >

virtual statet& static_analysist< T >::get_state ( locationt l )

inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 323 of file static_analysis.h.

◆ get_state() [2/2]

template<typename T >

virtual const statet& static_analysist< T >::get_state ( locationt l ) const

inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 332 of file static_analysis.h.

◆ has_location()

template<typename T >

virtual bool static_analysist< T >::has_location ( locationt l ) const

inlinevirtual

Implements static_analysis_baset.

Definition at line 314 of file static_analysis.h.

◆ make_temporary_state()

template<typename T >

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

inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 346 of file static_analysis.h.

◆ merge()

template<typename T >

virtual bool static_analysist< T >::merge	(	statet &	a,
		const statet &	b,
		locationt	to
	)

inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 341 of file static_analysis.h.

◆ merge_shared()

template<typename T >

virtual bool static_analysist< T >::merge_shared	(	statet &	,
		const statet &	,
		goto_programt::const_targett
	)

inlineprivatevirtual

Implements static_analysis_baset.

Reimplemented in concurrency_aware_static_analysist< T >.

Definition at line 374 of file static_analysis.h.

◆ operator[]() [1/2]

template<typename T >

T& static_analysist< T >::operator[] ( locationt l )

inline

Definition at line 290 of file static_analysis.h.

◆ operator[]() [2/2]

template<typename T >

const T& static_analysist< T >::operator[] ( locationt l ) const

inline

Definition at line 299 of file static_analysis.h.

Member Data Documentation

◆ state_map

template<typename T >

state_mapt static_analysist< T >::state_map

protected

Definition at line 321 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 Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Additional Inherited Members

Detailed Description

template<typename T> class static_analysist< T >

Member Typedef Documentation

◆ locationt

◆ state_mapt

Constructor & Destructor Documentation

◆ static_analysist()

Member Function Documentation

◆ clear()

◆ dummy()

◆ fixedpoint()

◆ generate_state()

◆ get_reference_set()

◆ get_state() [1/2]

◆ get_state() [2/2]

◆ has_location()

◆ make_temporary_state()

◆ merge()

◆ merge_shared()

◆ operator[]() [1/2]

◆ operator[]() [2/2]

Member Data Documentation

◆ state_map

template<typename T>
class static_analysist< T >