cprover
offset_entryt Class Reference

#include <write_stack_entry.h>

+ Inheritance diagram for offset_entryt:
+ Collaboration diagram for offset_entryt:

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. More...
 
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. More...
 
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. More...
 
- Public Member Functions inherited from write_stack_entryt
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. More...
 

Private Attributes

abstract_object_pointert offset
 

Detailed Description

Definition at line 43 of file write_stack_entry.h.

Constructor & Destructor Documentation

◆ offset_entryt()

offset_entryt::offset_entryt ( abstract_object_pointert  offset_value)
explicit

Definition at line 53 of file write_stack_entry.cpp.

Member Function Documentation

◆ adjust_access_type()

void offset_entryt::adjust_access_type ( exprt expr) const
overridevirtual

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.

◆ get_access_expr()

exprt offset_entryt::get_access_expr ( ) const
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.

Returns
The untyped expression to read this part of the stack

Implements write_stack_entryt.

Definition at line 69 of file write_stack_entry.cpp.

◆ try_squash_in()

bool offset_entryt::try_squash_in ( std::shared_ptr< const write_stack_entryt new_entry,
const abstract_environmentt enviroment,
const namespacet ns 
)
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

Parameters
new_entryThe new entry to combine with
enviromentThe enviroment to evalaute things in
nsThe global namespace
Returns
True if this stack entry and thew new entry were combined

Reimplemented from write_stack_entryt.

Definition at line 93 of file write_stack_entry.cpp.

Member Data Documentation

◆ offset

abstract_object_pointert offset_entryt::offset
private

Definition at line 55 of file write_stack_entry.h.


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