memory_snapshot_harness_generatort::entry_goto_locationt Struct Reference

User provided goto location: function name and (maybe) location number; the structure wraps this option with a parser. More...

#include <memory_snapshot_harness_generator.h>

Collaboration diagram for memory_snapshot_harness_generatort::entry_goto_locationt:

Public Member Functions
	entry_goto_locationt ()=delete
	entry_goto_locationt (irep_idt function_name)
	entry_goto_locationt (irep_idt function_name, unsigned location_number)
goto_programt::const_targett	find_first_corresponding_instruction (const goto_programt::instructionst &instructions) const
	Returns the first goto_programt::instructiont represented by this goto location, i.e. More...

Public Attributes
irep_idt	function_name
optionalt< unsigned >	location_number

Detailed Description

User provided goto location: function name and (maybe) location number; the structure wraps this option with a parser.

Definition at line 52 of file memory_snapshot_harness_generator.h.

Constructor & Destructor Documentation

entry_goto_locationt() [1/3]

memory_snapshot_harness_generatort::entry_goto_locationt::entry_goto_locationt ( )

delete

entry_goto_locationt() [2/3]

memory_snapshot_harness_generatort::entry_goto_locationt::entry_goto_locationt ( irep_idt  function_name )

inlineexplicit

Definition at line 58 of file memory_snapshot_harness_generator.h.

entry_goto_locationt() [3/3]

memory_snapshot_harness_generatort::entry_goto_locationt::entry_goto_locationt ( irep_idt  function_name, unsigned  location_number  )

inlineexplicit

Definition at line 62 of file memory_snapshot_harness_generator.h.

Member Function Documentation

find_first_corresponding_instruction()

goto_programt::const_targett memory_snapshot_harness_generatort::entry_goto_locationt::find_first_corresponding_instruction

(

const goto_programt::instructionst &

instructions

)

const

Returns the first goto_programt::instructiont represented by this goto location, i.e.

if there is no location number then the first instruction, otherwise the one with the right location number

Parameters

instructions

list of instructions to be searched

Returns

iterator to the right instruction (or end())

Definition at line 532 of file memory_snapshot_harness_generator.cpp.

Member Data Documentation

function_name

irep_idt memory_snapshot_harness_generatort::entry_goto_locationt::function_name

Definition at line 54 of file memory_snapshot_harness_generator.h.

location_number

optionalt<unsigned> memory_snapshot_harness_generatort::entry_goto_locationt::location_number

Definition at line 55 of file memory_snapshot_harness_generator.h.

---

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

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