|
CBMC
|
Symex Shadow Memory Instrumentation. More...
Include dependency graph for shadow_memory.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | shadow_memoryt |
| The shadow memory instrumentation performed during symbolic execution. More... | |
Macros | |
| #define | SHADOW_MEMORY_PREFIX "SM__" |
| #define | SHADOW_MEMORY_FIELD_DECL "field_decl" |
| #define | SHADOW_MEMORY_GLOBAL_SCOPE "_global" |
| #define | SHADOW_MEMORY_LOCAL_SCOPE "_local" |
| #define | SHADOW_MEMORY_GET_FIELD "get_field" |
| #define | SHADOW_MEMORY_SET_FIELD "set_field" |
| #define | SHADOW_MEMORY_SYMBOL_PREFIX "__SM" |
Symex Shadow Memory Instrumentation.
Definition in file shadow_memory.h.
| #define SHADOW_MEMORY_FIELD_DECL "field_decl" |
Definition at line 21 of file shadow_memory.h.
| #define SHADOW_MEMORY_GET_FIELD "get_field" |
Definition at line 24 of file shadow_memory.h.
| #define SHADOW_MEMORY_GLOBAL_SCOPE "_global" |
Definition at line 22 of file shadow_memory.h.
| #define SHADOW_MEMORY_LOCAL_SCOPE "_local" |
Definition at line 23 of file shadow_memory.h.
| #define SHADOW_MEMORY_PREFIX "SM__" |
Definition at line 20 of file shadow_memory.h.
| #define SHADOW_MEMORY_SET_FIELD "set_field" |
Definition at line 25 of file shadow_memory.h.
| #define SHADOW_MEMORY_SYMBOL_PREFIX "__SM" |
Definition at line 26 of file shadow_memory.h.