Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion. More...

#include <call_stack_history.h>

Inheritance diagram for call_stack_historyt:

Collaboration diagram for call_stack_historyt:

Classes
class	call_stack_entryt

Public Member Functions
	call_stack_historyt (locationt l)

	call_stack_historyt (locationt l, unsigned int rec_lim)

	call_stack_historyt (const call_stack_historyt &old)

step_returnt	step (locationt to, const trace_sett &others, trace_ptrt caller_hist) const override
	Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point.

bool	operator< (const ai_history_baset &op) const override
	The order for history_sett.

bool	operator== (const ai_history_baset &op) const override
	History objects should be comparable.

const locationt &	current_location (void) const override
	The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)

bool	should_widen (const ai_history_baset &other) const override
	Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way.

void	output (std::ostream &out) const override

Public Member Functions inherited from ai_history_baset
virtual	~ai_history_baset ()

virtual jsont	output_json (void) const

virtual xmlt	output_xml (void) const

Protected Types
typedef std::shared_ptr< const call_stack_entryt >	cse_ptrt

Protected Member Functions
bool	has_recursion_limit (void) const

	call_stack_historyt (cse_ptrt cur_stack, unsigned int rec_lim)

Protected Member Functions inherited from ai_history_baset
	ai_history_baset (locationt)
	Create a new history starting from a given location This is used to start the analysis from scratch PRECONDITION(l.is_dereferenceable());.

	ai_history_baset (const ai_history_baset &)

Protected Attributes
cse_ptrt	current_stack

unsigned int	recursion_limit

Additional Inherited Members
Public Types inherited from ai_history_baset
enum class	step_statust { NEW , MERGED , BLOCKED }

typedef goto_programt::const_targett	locationt

typedef std::shared_ptr< const ai_history_baset >	trace_ptrt
	History objects are intended to be immutable so they can be shared to reduce memory overhead.

typedef std::set< trace_ptrt, compare_historyt >	trace_sett

typedef std::pair< step_statust, trace_ptrt >	step_returnt

Static Public Attributes inherited from ai_history_baset
static const trace_ptrt	no_caller_history

Detailed Description

Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion.

Definition at line 20 of file call_stack_history.h.

Member Typedef Documentation

◆ cse_ptrt

typedef std::shared_ptr<const call_stack_entryt> call_stack_historyt::cse_ptrt

protected

Definition at line 24 of file call_stack_history.h.

Constructor & Destructor Documentation

◆ call_stack_historyt() [1/4]

call_stack_historyt::call_stack_historyt	(	cse_ptrt	cur_stack,
		unsigned int	rec_lim
	)

inlineprotected

Definition at line 53 of file call_stack_history.h.

◆ call_stack_historyt() [2/4]

call_stack_historyt::call_stack_historyt ( locationt l )

inlineexplicit

Definition at line 63 of file call_stack_history.h.

◆ call_stack_historyt() [3/4]

call_stack_historyt::call_stack_historyt	(	locationt	l,
		unsigned int	rec_lim
	)

inline

Definition at line 70 of file call_stack_history.h.

◆ call_stack_historyt() [4/4]

call_stack_historyt::call_stack_historyt ( const call_stack_historyt & old )

inline

Definition at line 77 of file call_stack_history.h.

Member Function Documentation

◆ current_location()

const locationt & call_stack_historyt::current_location ( void ) const

inlineoverridevirtual

The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)

Implements ai_history_baset.

Definition at line 92 of file call_stack_history.h.

◆ has_recursion_limit()

bool call_stack_historyt::has_recursion_limit ( void ) const

inlineprotected

Definition at line 48 of file call_stack_history.h.

◆ operator<()

bool call_stack_historyt::operator< ( const ai_history_baset & op ) const

overridevirtual

The order for history_sett.

Implements ai_history_baset.

Definition at line 144 of file call_stack_history.cpp.

◆ operator==()

bool call_stack_historyt::operator== ( const ai_history_baset & op ) const

overridevirtual

History objects should be comparable.

Implements ai_history_baset.

Definition at line 152 of file call_stack_history.cpp.

◆ output()

void call_stack_historyt::output ( std::ostream & out ) const

overridevirtual

Reimplemented from ai_history_baset.

Definition at line 160 of file call_stack_history.cpp.

◆ should_widen()

bool call_stack_historyt::should_widen ( const ai_history_baset & other ) const

inlineoverridevirtual

Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way.

However it could be used in other ways (such as the transformer). The key idea is that the history tracks / should know when to widen and when to continue.

Reimplemented from ai_history_baset.

Definition at line 100 of file call_stack_history.h.

◆ step()

ai_history_baset::step_returnt call_stack_historyt::step	(	locationt	to,
		const trace_sett &	others,
		trace_ptrt	caller_hist
	)		const

overridevirtual

Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point.

In the case of function call return it is also given the full history of the caller. This allows function-local histories as they can "pick up" the state from before the call when computing the return edge.

PRECONDITION(to.id_dereferenceable()); PRECONDITION(to in goto_program.get_successors(current_location()) || current_location()->is_function_call() || current_location()->is_end_function()); PRECONDITION(caller_hist == no_caller_history || current_location()->is_end_function);

Step may do one of three things :

Create a new history object and return a pointer to it This will force the analyser to continue regardless of domain changes POSTCONDITION(IMPLIES(result.first == step_statust::NEW, result.second.use_count() == 1 ));
Merge with an existing history This means the analyser will only continue if the domain is updated POSTCONDITION(IMPLIES(result.first == step_statust::MERGED, result.second is an element of others));
Block this flow of execution This indicates the transition is impossible (returning to a location other than the call location) or undesireable (omitting some traces) POSTCONDITION(IMPLIES(result.first == BLOCKED, result.second == nullptr()));

Implements ai_history_baset.

Definition at line 14 of file call_stack_history.cpp.

Member Data Documentation

◆ current_stack

cse_ptrt call_stack_historyt::current_stack

protected

Definition at line 39 of file call_stack_history.h.

◆ recursion_limit

unsigned int call_stack_historyt::recursion_limit

protected

Definition at line 46 of file call_stack_history.h.

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

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

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ cse_ptrt

Constructor & Destructor Documentation

◆ call_stack_historyt() [1/4]

◆ call_stack_historyt() [2/4]

◆ call_stack_historyt() [3/4]

◆ call_stack_historyt() [4/4]

Member Function Documentation

◆ current_location()

◆ has_recursion_limit()

◆ operator<()

◆ operator==()

◆ output()

◆ should_widen()

◆ step()

Member Data Documentation

◆ current_stack

◆ recursion_limit