CBMC
Loading...
Searching...
No Matches
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:
[フレーム]
[legend]

Classes

struct   shadowed_addresst
 

Public Attributes

shadow_memory_field_definitionst  fields
  The available shadow memory field definitions.
 
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:

AltStyle によって変換されたページ (->オリジナル) /