Public Member Functions

Try to combine a new stack element with the current top of the stack.

Detailed Description

Definition at line 20 of file write_stack_entry.h.

virtual write_stack_entryt::~write_stack_entryt ( )

virtualdefault

virtual std::pair< exprt, bool > write_stack_entryt::get_access_expr ( ) const

pure virtual

bool write_stack_entryt::try_squash_in ( std::shared_ptr< const write_stack_entryt > new_entry,

const abstract_environmentt & enviroment,

const namespacet & ns

)

virtual

Try to combine a new stack element with the current top of the stack.

Parameters: new_entry The new entry to combine with

enviroment The enviroment to evalaute things in

ns The global namespace

Reimplemented in offset_entryt.

Definition at line 22 of file write_stack_entry.cpp.

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

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