CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
shadow_memory_field_definitions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symex Shadow Memory Instrumentation
4
5Author: 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
32
33#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_FIELD_DEFINITIONS_H
The shadow memory field definitions.
field_definitiont global_fields
Field definitions for global-scope fields.
field_definitiont local_fields
Field definitions for local-scope fields.
std::map< irep_idt, exprt > field_definitiont
A field definition mapping a field name to its initial value.