cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
expr.h
goto-symex
shadow_memory_field_definitions.h
Generated by
1.17.0