cprover
|
#include <write_stack_entry.h>
Public Member Functions | |
simple_entryt (exprt expr) | |
Build a simple entry based off a single expression. | |
exprt | get_access_expr () const override |
Get the expression part needed to read this stack entry. | |
void | adjust_access_type (exprt &expr) const override |
For a simple entry, no type adjustment is needed for the access expression. | |
![]() | |
virtual | ~write_stack_entryt ()=default |
virtual exprt | get_access_expr () const =0 |
virtual void | adjust_access_type (exprt &expr) const =0 |
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. | |
Private Attributes | |
exprt | simple_entry |
Definition at line 32 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 |
For a simple entry, no type adjustment is needed for the access expression.
Implements write_stack_entryt.
Definition at line 49 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 40 of file write_stack_entry.h.