shadow_memory_field_definitionst Class Reference
The shadow memory field definitions. More...
#include <shadow_memory_field_definitions.h>
Collaboration diagram for shadow_memory_field_definitionst:Public Types | |
| using | field_definitiont = std::map< irep_idt, exprt > |
| A field definition mapping a field name to its initial value. More... | |
Public Attributes | |
| field_definitiont | global_fields |
| Field definitions for global-scope fields. More... | |
| field_definitiont | local_fields |
| Field definitions for local-scope fields. More... | |
Detailed Description
The shadow memory field definitions.
Definition at line 20 of file shadow_memory_field_definitions.h.
Member Typedef Documentation
◆ field_definitiont
| using shadow_memory_field_definitionst::field_definitiont = std::map<irep_idt, exprt> |
A field definition mapping a field name to its initial value.
Definition at line 24 of file shadow_memory_field_definitions.h.
Member Data Documentation
◆ global_fields
| field_definitiont shadow_memory_field_definitionst::global_fields |
Field definitions for global-scope fields.
Definition at line 27 of file shadow_memory_field_definitions.h.
◆ local_fields
| field_definitiont shadow_memory_field_definitionst::local_fields |
Field definitions for local-scope fields.
Definition at line 30 of file shadow_memory_field_definitions.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-symex/shadow_memory_field_definitions.h
