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 |
optionalt< unsigned > | location_number |
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.
|
delete |
|
inlineexplicit |
Definition at line 58 of file memory_snapshot_harness_generator.h.
|
inlineexplicit |
Definition at line 62 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 |
end()
) 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 54 of file memory_snapshot_harness_generator.h.
Definition at line 55 of file memory_snapshot_harness_generator.h.