#include <flow_insensitive_analysis.h>

Inheritance diagram for flow_insensitive_analysis_baset:

Collaboration diagram for flow_insensitive_analysis_baset:

Public Types
typedef flow_insensitive_abstract_domain_baset	statet

typedef goto_programt::const_targett	locationt

Public Member Functions
bool	seen (const locationt &l)

	flow_insensitive_analysis_baset (const namespacet &_ns)

virtual void	initialize (const goto_programt &)

virtual void	initialize (const goto_functionst &)

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

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)

Public Attributes
std::set< locationt, goto_programt::target_less_than >	seen_locations

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

Protected Types
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

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

virtual statet &	get_state ()=0

virtual const statet &	get_state () const =0

virtual void	get_reference_set (const exprt &expr, expr_sett &expr_set)=0

Static Protected Member Functions
static locationt	successor (locationt l)

Protected Attributes
const namespacet &	ns

functions_donet	functions_done

recursion_sett	recursion_set

bool	initialized

Detailed Description

Definition at line 90 of file flow_insensitive_analysis.h.

Member Typedef Documentation

◆ expr_sett

typedef flow_insensitive_abstract_domain_baset::expr_sett flow_insensitive_analysis_baset::expr_sett

protected

Definition at line 226 of file flow_insensitive_analysis.h.

◆ functions_donet

typedef std::set<irep_idt> flow_insensitive_analysis_baset::functions_donet

protected

Definition at line 196 of file flow_insensitive_analysis.h.

◆ locationt

typedef goto_programt::const_targett flow_insensitive_analysis_baset::locationt

Definition at line 94 of file flow_insensitive_analysis.h.

◆ recursion_sett

typedef std::set<irep_idt> flow_insensitive_analysis_baset::recursion_sett

protected

Definition at line 199 of file flow_insensitive_analysis.h.

◆ statet

typedef flow_insensitive_abstract_domain_baset flow_insensitive_analysis_baset::statet

Definition at line 93 of file flow_insensitive_analysis.h.

◆ working_sett

typedef std::priority_queue< locationt, std::vector<locationt>, goto_programt::target_less_than> flow_insensitive_analysis_baset::working_sett

protected

Definition at line 162 of file flow_insensitive_analysis.h.

Constructor & Destructor Documentation

◆ flow_insensitive_analysis_baset()

flow_insensitive_analysis_baset::flow_insensitive_analysis_baset ( const namespacet & _ns )

inlineexplicit

Definition at line 105 of file flow_insensitive_analysis.h.

◆ ~flow_insensitive_analysis_baset()

virtual flow_insensitive_analysis_baset::~flow_insensitive_analysis_baset ( )

inlinevirtual

Definition at line 137 of file flow_insensitive_analysis.h.

Member Function Documentation

◆ clear()

virtual void flow_insensitive_analysis_baset::clear ( void )

inlinevirtual

Reimplemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

Definition at line 141 of file flow_insensitive_analysis.h.

◆ do_function_call()

bool flow_insensitive_analysis_baset::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

Definition at line 190 of file flow_insensitive_analysis.cpp.

◆ do_function_call_rec()

bool flow_insensitive_analysis_baset::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
	)

protected

Definition at line 273 of file flow_insensitive_analysis.cpp.

◆ fixedpoint() [1/2]

void flow_insensitive_analysis_baset::fixedpoint ( const goto_functionst & goto_functions )

protected

Definition at line 379 of file flow_insensitive_analysis.cpp.

◆ fixedpoint() [2/2]

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

protected

Definition at line 96 of file flow_insensitive_analysis.cpp.

◆ get_next()

flow_insensitive_analysis_baset::locationt flow_insensitive_analysis_baset::get_next ( working_sett & working_set )

protected

Definition at line 80 of file flow_insensitive_analysis.cpp.

◆ get_reference_set()

virtual void flow_insensitive_analysis_baset::get_reference_set	(	const exprt &	expr,
		expr_sett &	expr_set
	)

protectedpure virtual

Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

◆ get_state() [1/2]

virtual const statet& flow_insensitive_analysis_baset::get_state ( ) const

protectedpure virtual

Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

◆ get_state() [2/2]

virtual statet& flow_insensitive_analysis_baset::get_state ( )

protectedpure virtual

Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

◆ initialize() [1/2]

virtual void flow_insensitive_analysis_baset::initialize ( const goto_functionst & )

inlinevirtual

Reimplemented in value_set_analysis_fit.

Definition at line 119 of file flow_insensitive_analysis.h.

◆ initialize() [2/2]

virtual void flow_insensitive_analysis_baset::initialize ( const goto_programt & )

inlinevirtual

Reimplemented in value_set_analysis_fit.

Definition at line 111 of file flow_insensitive_analysis.h.

◆ operator()() [1/2]

void flow_insensitive_analysis_baset::operator() ( const goto_functionst & goto_functions )

virtual

Definition at line 43 of file flow_insensitive_analysis.cpp.

◆ operator()() [2/2]

void flow_insensitive_analysis_baset::operator()	(	const irep_idt &	function_id,
		const goto_programt &	goto_program
	)

virtual

Definition at line 50 of file flow_insensitive_analysis.cpp.

◆ output() [1/2]

void flow_insensitive_analysis_baset::output	(	const goto_functionst &	goto_functions,
		std::ostream &	out
	)

virtual

Definition at line 58 of file flow_insensitive_analysis.cpp.

◆ output() [2/2]

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

virtual

Definition at line 71 of file flow_insensitive_analysis.cpp.

◆ put_in_working_set()

void flow_insensitive_analysis_baset::put_in_working_set	(	working_sett &	working_set,
		locationt	l
	)

inlineprotected

Definition at line 166 of file flow_insensitive_analysis.h.

◆ seen()

bool flow_insensitive_analysis_baset::seen ( const locationt & l )

inline

Definition at line 100 of file flow_insensitive_analysis.h.

◆ successor()

static locationt flow_insensitive_analysis_baset::successor ( locationt l )

inlinestaticprotected

Definition at line 190 of file flow_insensitive_analysis.h.

◆ update() [1/2]

void flow_insensitive_analysis_baset::update ( const goto_functionst & goto_functions )

virtual

Definition at line 394 of file flow_insensitive_analysis.cpp.

◆ update() [2/2]

void flow_insensitive_analysis_baset::update ( const goto_programt & goto_program )

virtual

Definition at line 399 of file flow_insensitive_analysis.cpp.

◆ visit()

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

protected

Definition at line 125 of file flow_insensitive_analysis.cpp.

Member Data Documentation

◆ functions_done

functions_donet flow_insensitive_analysis_baset::functions_done

protected

Definition at line 197 of file flow_insensitive_analysis.h.

◆ initialized

bool flow_insensitive_analysis_baset::initialized

protected

Definition at line 202 of file flow_insensitive_analysis.h.

◆ ns

const namespacet& flow_insensitive_analysis_baset::ns

protected

Definition at line 156 of file flow_insensitive_analysis.h.

◆ recursion_set

recursion_sett flow_insensitive_analysis_baset::recursion_set

protected

Definition at line 200 of file flow_insensitive_analysis.h.

◆ seen_locations

std::set<locationt, goto_programt::target_less_than> flow_insensitive_analysis_baset::seen_locations

Definition at line 96 of file flow_insensitive_analysis.h.

◆ statistics

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

Definition at line 98 of file flow_insensitive_analysis.h.

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

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

Public Types

Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ expr_sett

◆ functions_donet

◆ locationt

◆ recursion_sett

◆ statet

◆ working_sett

Constructor & Destructor Documentation

◆ flow_insensitive_analysis_baset()

◆ ~flow_insensitive_analysis_baset()

Member Function Documentation

◆ clear()

◆ do_function_call()

◆ do_function_call_rec()

◆ fixedpoint() [1/2]

◆ fixedpoint() [2/2]

◆ get_next()

◆ get_reference_set()

◆ get_state() [1/2]

◆ get_state() [2/2]

◆ initialize() [1/2]

◆ initialize() [2/2]

◆ operator()() [1/2]

◆ operator()() [2/2]

◆ output() [1/2]

◆ output() [2/2]

◆ put_in_working_set()

◆ seen()

◆ successor()

◆ update() [1/2]

◆ update() [2/2]

◆ visit()

Member Data Documentation

◆ functions_done

◆ initialized

◆ ns

◆ recursion_set

◆ seen_locations

◆ statistics