|
cprover
|
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>
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. | |
Public Attributes | |
| irep_idt | function_name |
| std::optional< unsigned > | location_number |
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.
|
delete |
|
inlineexplicit |
Definition at line 59 of file memory_snapshot_harness_generator.h.
|
inlineexplicit |
Definition at line 63 of file memory_snapshot_harness_generator.h.
| 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
| instructions | list of instructions to be searched |
Definition at line 531 of file memory_snapshot_harness_generator.cpp.
| irep_idt memory_snapshot_harness_generatort::entry_goto_locationt::function_name |
Definition at line 55 of file memory_snapshot_harness_generator.h.
| std::optional<unsigned> memory_snapshot_harness_generatort::entry_goto_locationt::location_number |
Definition at line 56 of file memory_snapshot_harness_generator.h.