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 |
| std::optional< 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 53 of file memory_snapshot_harness_generator.h.
Constructor & Destructor Documentation
◆ entry_goto_locationt() [1/3]
|
delete |
◆ entry_goto_locationt() [2/3]
|
inlineexplicit |
Definition at line 59 of file memory_snapshot_harness_generator.h.
◆ entry_goto_locationt() [3/3]
|
inlineexplicit |
Definition at line 63 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 531 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 55 of file memory_snapshot_harness_generator.h.
◆ location_number
| std::optional<unsigned> memory_snapshot_harness_generatort::entry_goto_locationt::location_number |
Definition at line 56 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
