Loading...

Searching...

No Matches

write_stackt Class Reference

#include <write_stack.h>

+ Collaboration diagram for write_stackt:

[フレーム]

[legend]

Public Types

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

Public Member Functions

write_stackt ()

Build a topstack.

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

Construct a write stack from an expression.

exprt to_expression () const

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

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.

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.

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.

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.

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.

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.

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 class 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

write_stackt
Generated by doxygen 1.9.8