CBMC
Public Member Functions | Private Attributes | List of all members
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)
 
std::pair< exprt, bool > get_access_expr () const override
 Get the expression part needed to read this stack entry. 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
 

Private Attributes

abstract_object_pointert offset
 

Detailed Description

Definition at line 41 of file write_stack_entry.h.

Constructor & Destructor Documentation

◆ offset_entryt()

offset_entryt::offset_entryt ( abstract_object_pointert  offset_value)
explicit

Definition at line 48 of file write_stack_entry.cpp.

Member Function Documentation

◆ get_access_expr()

std::pair< exprt, bool > offset_entryt::get_access_expr ( ) const
overridevirtual

Get the expression part needed to read this stack entry.

For offset entries this is the offset for an index expression.

Returns
The offset expression to read this part of the stack and true

Implements write_stack_entryt.

Definition at line 61 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 73 of file write_stack_entry.cpp.

Member Data Documentation

◆ offset

abstract_object_pointert offset_entryt::offset
private

Definition at line 52 of file write_stack_entry.h.

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