memory_snapshot_harness_generatort::entry_source_locationt Struct Reference

User provided source location: file name and line number; the structure wraps this option with a parser. More...

#include <memory_snapshot_harness_generator.h>

Collaboration diagram for memory_snapshot_harness_generatort::entry_source_locationt:

Public Member Functions
	entry_source_locationt ()=delete
	entry_source_locationt (irep_idt file_name, unsigned line_number)
std::pair< goto_programt::const_targett, size_t >	find_first_corresponding_instruction (const goto_programt::instructionst &instructions) const
	Returns the first goto_programt::instructiont represented by this source location, i.e.

Public Attributes
irep_idt	file_name
unsigned	line_number

Detailed Description

User provided source location: file name and line number; the structure wraps this option with a parser.

Definition at line 87 of file memory_snapshot_harness_generator.h.

Constructor & Destructor Documentation

entry_source_locationt() [1/2]

memory_snapshot_harness_generatort::entry_source_locationt::entry_source_locationt ( )

delete

entry_source_locationt() [2/2]

memory_snapshot_harness_generatort::entry_source_locationt::entry_source_locationt ( irep_idt  file_name, unsigned  line_number  )

inlineexplicit

Definition at line 93 of file memory_snapshot_harness_generator.h.

Member Function Documentation

find_first_corresponding_instruction()

std::pair< goto_programt::const_targett, size_t > memory_snapshot_harness_generatort::entry_source_locationt::find_first_corresponding_instruction

(

const goto_programt::instructionst &

instructions

)

const

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

one with the same file name and line number

Parameters

instructions

list of instructions to be searched

Returns

<iterator to the right instruction (or `end()`), distance to `line_number`>

Definition at line 547 of file memory_snapshot_harness_generator.cpp.

Member Data Documentation

file_name

irep_idt memory_snapshot_harness_generatort::entry_source_locationt::file_name

Definition at line 89 of file memory_snapshot_harness_generator.h.

line_number

unsigned memory_snapshot_harness_generatort::entry_source_locationt::line_number

Definition at line 90 of file memory_snapshot_harness_generator.h.

---

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

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