Include dependency graph for structured_trace_util.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| struct | default_trace_stept |
Enumerations | |
| enum | default_step_kindt { default_step_kindt::LOCATION_ONLY, default_step_kindt::LOOP_HEAD } |
| There are two kinds of step for location markers - location-only and loop-head (for locations associated with the first step of a loop). More... | |
Functions | |
| default_step_kindt | default_step_kind (const goto_programt::instructiont &instruction) |
| Identify for a given instruction whether it is a loophead or just a location. More... | |
| std::string | default_step_name (const default_step_kindt &step_type) |
| Turns a default_step_kindt into a string that can be used in the trace. More... | |
| optionalt< default_trace_stept > | default_step (const goto_trace_stept &step, const source_locationt &previous_source_location) |
Detailed Description
Utilities for printing location info steps in the trace in a format agnostic way
Definition in file structured_trace_util.h.
Enumeration Type Documentation
◆ default_step_kindt
|
strong |
There are two kinds of step for location markers - location-only and loop-head (for locations associated with the first step of a loop).
| Enumerator | |
|---|---|
| LOCATION_ONLY | |
| LOOP_HEAD | |
Definition at line 20 of file structured_trace_util.h.
Function Documentation
◆ default_step()
| optionalt<default_trace_stept> default_step | ( | const goto_trace_stept & | step, |
| const source_locationt & | previous_source_location | ||
| ) |
Definition at line 39 of file structured_trace_util.cpp.
◆ default_step_kind()
| default_step_kindt default_step_kind | ( | const goto_programt::instructiont & | instruction | ) |
Identify for a given instruction whether it is a loophead or just a location.
Loopheads are determined by whether there is backwards jump to them. This matches the loop detection used for loop IDs
- Parameters
-
instruction The instruction to inspect.
- Returns
- LOOP_HEAD if this is a loop head, otherwise LOCATION_ONLY
Definition at line 17 of file structured_trace_util.cpp.
◆ default_step_name()
| std::string default_step_name | ( | const default_step_kindt & | step_type | ) |
Turns a default_step_kindt into a string that can be used in the trace.
- Parameters
-
step_type The kind of step, deduced from default_step_kind
- Returns
- Either "loop-head" or "location-only"
Definition at line 27 of file structured_trace_util.cpp.
