#include <write_stack.h>

Collaboration diagram for write_stackt:

Public Types
typedef std::vector< std::shared_ptr< write_stack_entryt > >	continuation_stack_storet

Public Member Functions
	write_stackt ()
	Build a topstack. More...

	write_stackt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Construct a write stack from an expression. More...

exprt	to_expression () const
	Convert the stack to an expression that can be used to write to. More...

size_t	depth () const

exprt	target_expression (size_t depth) const

exprt	offset_expression () const

bool	is_top_value () const
	Is the stack representing an unknown value and hence can't be written to or read from. More...

Private Types
enum class	integral_resultt { LHS_INTEGRAL , RHS_INTEGRAL , NEITHER_INTEGRAL }

Private Member Functions
void	construct_stack_to_pointer (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Add to the stack the elements to get to a pointer. More...

void	construct_stack_to_lvalue (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Construct a stack up to a specific l-value (i.e. More...

void	construct_stack_to_array_index (const index_exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Construct a stack for an array position l-value. More...

void	add_to_stack (std::shared_ptr< write_stack_entryt > entry_pointer, const abstract_environmentt environment, const namespacet &ns)
	Add an element to the top of the stack. More...

Static Private Member Functions
static integral_resultt	get_which_side_integral (const exprt &expr, exprt &out_base_expr, exprt &out_integral_expr)
	Utility function to find out which side of a binary operation has an integral type, if any. More...

Private Attributes
continuation_stack_storet	stack

bool	top_stack

Detailed Description

Definition at line 25 of file write_stack.h.

Member Typedef Documentation

◆ continuation_stack_storet

typedef std::vector<std::shared_ptr<write_stack_entryt> > write_stackt::continuation_stack_storet

Definition at line 29 of file write_stack.h.

Member Enumeration Documentation

◆ integral_resultt

enum write_stackt::integral_resultt

strongprivate

Enumerator
LHS_INTEGRAL
RHS_INTEGRAL
NEITHER_INTEGRAL

Definition at line 66 of file write_stack.h.

Constructor & Destructor Documentation

◆ write_stackt() [1/2]

write_stackt::write_stackt ( )

Build a topstack.

Definition at line 26 of file write_stack.cpp.

◆ write_stackt() [2/2]

write_stackt::write_stackt	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

Construct a write stack from an expression.

Parameters

expr	The expression to represent
environment	The environment to evaluate any expressions in
ns	The global namespace

Definition at line 34 of file write_stack.cpp.

Member Function Documentation

◆ add_to_stack()

void write_stackt::add_to_stack	(	std::shared_ptr< write_stack_entryt >	entry_pointer,
		const abstract_environmentt	environment,
		const namespacet &	ns
	)

private

Add an element to the top of the stack.

This will squash in with the top element if possible.

Parameters

entry_pointer	The new element for the stack.
environment	The environment to evaluate any expressions in
ns	The global namespace

Definition at line 235 of file write_stack.cpp.

◆ construct_stack_to_array_index()

void write_stackt::construct_stack_to_array_index	(	const index_exprt &	index_expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

private

Construct a stack for an array position l-value.

Parameters

index_expr	The index expression to construct to.
environment	The environment to evaluate any expressions in
ns	The global namespace

Definition at line 161 of file write_stack.cpp.

◆ construct_stack_to_lvalue()

void write_stackt::construct_stack_to_lvalue	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

private

Construct a stack up to a specific l-value (i.e.

symbol or position in an array or struct)

Parameters

expr	The expression representing a l-value
environment	The environment to evaluate any expressions in
ns	The global namespace

Definition at line 129 of file write_stack.cpp.

◆ construct_stack_to_pointer()

void write_stackt::construct_stack_to_pointer	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

private

Add to the stack the elements to get to a pointer.

Parameters

expr	An expression of type pointer to construct the stack to
environment	The environment to evaluate any expressions in
ns	The global namespace

Definition at line 60 of file write_stack.cpp.

◆ depth()

size_t write_stackt::depth ( ) const

Definition at line 194 of file write_stack.cpp.

◆ get_which_side_integral()

write_stackt::integral_resultt write_stackt::get_which_side_integral	(	const exprt &	expr,
		exprt &	out_base_expr,
		exprt &	out_integral_expr
	)

staticprivate

Utility function to find out which side of a binary operation has an integral type, if any.

Parameters

	expr	The (binary) expression to evaluate.
[out]	out_base_expr	The sub-expression which is not integral typed
[out]	out_integral_expr	The subexpression which is integraled typed.

Returns: : An enum specifying whether the integral type is the LHS (op0), RHS (op1) or neither.

Definition at line 255 of file write_stack.cpp.

◆ is_top_value()

bool write_stackt::is_top_value ( ) const

Is the stack representing an unknown value and hence can't be written to or read from.

Returns: True if the stack is top.

Definition at line 225 of file write_stack.cpp.

◆ offset_expression()

exprt write_stackt::offset_expression ( ) const

Definition at line 205 of file write_stack.cpp.

◆ target_expression()

exprt write_stackt::target_expression ( size_t depth ) const

Definition at line 199 of file write_stack.cpp.

◆ to_expression()

exprt write_stackt::to_expression ( ) const

Convert the stack to an expression that can be used to write to.

Returns: The expression representing the stack, with nil_exprt expressions for top elements.

Definition at line 176 of file write_stack.cpp.

Member Data Documentation

◆ stack

continuation_stack_storet write_stackt::stack

private

Definition at line 78 of file write_stack.h.

◆ top_stack

bool write_stackt::top_stack

private

Definition at line 79 of file write_stack.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/write_stack.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/write_stack.cpp

Public Types

Public Member Functions

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ continuation_stack_storet

Member Enumeration Documentation

◆ integral_resultt

Constructor & Destructor Documentation

◆ write_stackt() [1/2]

◆ write_stackt() [2/2]

Member Function Documentation

◆ add_to_stack()

◆ construct_stack_to_array_index()

◆ construct_stack_to_lvalue()

◆ construct_stack_to_pointer()

◆ depth()

◆ get_which_side_integral()

◆ is_top_value()

◆ offset_expression()

◆ target_expression()

◆ to_expression()

Member Data Documentation

◆ stack

◆ top_stack