memory_snapshot_harness_generatort::entry_locationt Struct Reference

Wraps the information needed to identify the entry point. More...

#include <memory_snapshot_harness_generator.h>

Collaboration diagram for memory_snapshot_harness_generatort::entry_locationt:

Public Member Functions
	entry_locationt ()=default
	entry_locationt (irep_idt function_name, goto_programt::const_targett start_instruction)

Public Attributes
irep_idt	function_name
goto_programt::const_targett	start_instruction

Detailed Description

Wraps the information needed to identify the entry point.

Initializes via either entry_goto_locationt or entry_source_locationt

Definition at line 116 of file memory_snapshot_harness_generator.h.

Constructor & Destructor Documentation

entry_locationt() [1/2]

memory_snapshot_harness_generatort::entry_locationt::entry_locationt ( )

default

entry_locationt() [2/2]

memory_snapshot_harness_generatort::entry_locationt::entry_locationt ( irep_idt  function_name, goto_programt::const_targett  start_instruction  )

inlineexplicit

Definition at line 122 of file memory_snapshot_harness_generator.h.

Member Data Documentation

function_name

irep_idt memory_snapshot_harness_generatort::entry_locationt::function_name

Definition at line 118 of file memory_snapshot_harness_generator.h.

start_instruction

goto_programt::const_targett memory_snapshot_harness_generatort::entry_locationt::start_instruction

Definition at line 119 of file memory_snapshot_harness_generator.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-harness/memory_snapshot_harness_generator.h