CBMC
Classes | Public Attributes | List of all members
shadow_memory_statet Class Reference

The state maintained by the shadow memory instrumentation during symbolic execution. More...

#include <shadow_memory_state.h>

+ Collaboration diagram for shadow_memory_statet:

Classes

struct  shadowed_addresst
 

Public Attributes

shadow_memory_field_definitionst fields
 The available shadow memory field definitions. More...
 
std::map< irep_idt, std::vector< shadowed_addresst > > address_fields
 

Detailed Description

The state maintained by the shadow memory instrumentation during symbolic execution.

Definition at line 25 of file shadow_memory_state.h.

Member Data Documentation

◆ address_fields

std::map<irep_idt, std::vector<shadowed_addresst> > shadow_memory_statet::address_fields

Definition at line 38 of file shadow_memory_state.h.

◆ fields

shadow_memory_field_definitionst shadow_memory_statet::fields

The available shadow memory field definitions.

Definition at line 29 of file shadow_memory_state.h.

The documentation for this class was generated from the following file: