shadow_memory_field_definitionst Class Reference

The shadow memory field definitions. More...

#include <shadow_memory_field_definitions.h>

Collaboration diagram for shadow_memory_field_definitionst:

Public Types
using	field_definitiont = std::map< irep_idt, exprt >
	A field definition mapping a field name to its initial value.

Public Attributes
field_definitiont	global_fields
	Field definitions for global-scope fields.
field_definitiont	local_fields
	Field definitions for local-scope fields.

Detailed Description

The shadow memory field definitions.

Definition at line 20 of file shadow_memory_field_definitions.h.

Member Typedef Documentation

field_definitiont

using shadow_memory_field_definitionst::field_definitiont = std::map<irep_idt, exprt>

A field definition mapping a field name to its initial value.

Definition at line 24 of file shadow_memory_field_definitions.h.

Member Data Documentation

global_fields

field_definitiont shadow_memory_field_definitionst::global_fields

Field definitions for global-scope fields.

Definition at line 27 of file shadow_memory_field_definitions.h.

local_fields

field_definitiont shadow_memory_field_definitionst::local_fields

Field definitions for local-scope fields.

Definition at line 30 of file shadow_memory_field_definitions.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-symex/shadow_memory_field_definitions.h