CBMC
|
#include <write_stack_entry.h>
Public Member Functions | |
simple_entryt (exprt expr) | |
Build a simple entry based off a single expression. More... | |
std::pair< exprt, bool > | get_access_expr () const override |
Get the expression part needed to read this stack entry. More... | |
Public Member Functions inherited from write_stack_entryt | |
virtual | ~write_stack_entryt ()=default |
virtual bool | try_squash_in (std::shared_ptr< const write_stack_entryt > new_entry, const abstract_environmentt &enviroment, const namespacet &ns) |
Try to combine a new stack element with the current top of the stack. More... | |
Private Attributes | |
exprt | simple_entry |
Definition at line 31 of file write_stack_entry.h.
|
explicit |
Build a simple entry based off a single expression.
expr | The expression being represented |
Definition at line 32 of file write_stack_entry.cpp.
|
overridevirtual |
Get the expression part needed to read this stack entry.
For simple expressions this is just the expression itself.
Implements write_stack_entryt.
Definition at line 43 of file write_stack_entry.cpp.
|
private |
Definition at line 38 of file write_stack_entry.h.