cprover
|
#include <write_stack_entry.h>
Public Member Functions | |
offset_entryt (abstract_object_pointert offset_value) | |
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 an offset entry, the type of the access expression can only be determined once the access expression has been completed with the next entry on the write stack. | |
bool | try_squash_in (std::shared_ptr< const write_stack_entryt > new_entry, const abstract_environmentt &enviroment, const namespacet &ns) override |
Try to combine a new stack element with the current top of the stack. | |
![]() | |
virtual | ~write_stack_entryt ()=default |
Private Attributes | |
abstract_object_pointert | offset |
Definition at line 43 of file write_stack_entry.h.
|
explicit |
Definition at line 53 of file write_stack_entry.cpp.
For an offset entry, the type of the access expression can only be determined once the access expression has been completed with the next entry on the write stack.
Implements write_stack_entryt.
Definition at line 80 of file write_stack_entry.cpp.
|
overridevirtual |
Get the expression part needed to read this stack entry.
For offset entries this is an index expression with the index() part the offset. It is important to note that the returned index_exprt does not have a type, so it will be necessary for the caller to update the type whenever the index expression is completed using adjust_access_type
on the resulting exprt.
Implements write_stack_entryt.
Definition at line 69 of file write_stack_entry.cpp.
|
overridevirtual |
Try to combine a new stack element with the current top of the stack.
This will succeed if they are both offsets as we can combine these offsets into the sum of the offsets
new_entry | The new entry to combine with |
enviroment | The enviroment to evalaute things in |
ns | The global namespace |
Reimplemented from write_stack_entryt.
Definition at line 93 of file write_stack_entry.cpp.
|
private |
Definition at line 55 of file write_stack_entry.h.