CBMC
shadow_memory.h File Reference

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"
 

Detailed Description

Symex Shadow Memory Instrumentation.

Definition in file shadow_memory.h.

Macro Definition Documentation

◆ SHADOW_MEMORY_FIELD_DECL

#define SHADOW_MEMORY_FIELD_DECL   "field_decl"

Definition at line 21 of file shadow_memory.h.

◆ SHADOW_MEMORY_GET_FIELD

#define SHADOW_MEMORY_GET_FIELD   "get_field"

Definition at line 24 of file shadow_memory.h.

◆ SHADOW_MEMORY_GLOBAL_SCOPE

#define SHADOW_MEMORY_GLOBAL_SCOPE   "_global"

Definition at line 22 of file shadow_memory.h.

◆ SHADOW_MEMORY_LOCAL_SCOPE

#define SHADOW_MEMORY_LOCAL_SCOPE   "_local"

Definition at line 23 of file shadow_memory.h.

◆ SHADOW_MEMORY_PREFIX

#define SHADOW_MEMORY_PREFIX   "SM__"

Definition at line 20 of file shadow_memory.h.

◆ SHADOW_MEMORY_SET_FIELD

#define SHADOW_MEMORY_SET_FIELD   "set_field"

Definition at line 25 of file shadow_memory.h.

◆ SHADOW_MEMORY_SYMBOL_PREFIX

#define SHADOW_MEMORY_SYMBOL_PREFIX   "__SM"

Definition at line 26 of file shadow_memory.h.