CBMC
shadow_memory_field_definitions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symex Shadow Memory Instrumentation
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_FIELD_DEFINITIONS_H
13 #define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_FIELD_DEFINITIONS_H
14 
15 #include <util/expr.h>
16 
17 #include <map>
18 
20 class shadow_memory_field_definitionst
21 {
22 public:
24  using field_definitiont = std::map<irep_idt, exprt>;
25 
27  field_definitiont global_fields;
28 
30  field_definitiont local_fields;
31 };
32 
33 #endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_FIELD_DEFINITIONS_H
shadow_memory_field_definitionst
The shadow memory field definitions.
Definition: shadow_memory_field_definitions.h:21
shadow_memory_field_definitionst::global_fields
field_definitiont global_fields
Field definitions for global-scope fields.
Definition: shadow_memory_field_definitions.h:27
shadow_memory_field_definitionst::local_fields
field_definitiont local_fields
Field definitions for local-scope fields.
Definition: shadow_memory_field_definitions.h:30
shadow_memory_field_definitionst::field_definitiont
std::map< irep_idt, exprt > field_definitiont
A field definition mapping a field name to its initial value.
Definition: shadow_memory_field_definitions.h:24