CBMC
structured_trace_util.cpp File Reference

Utilities for printing location info steps in the trace in a format agnostic way. More...

#include "structured_trace_util.h"
#include "goto_trace.h"
#include <algorithm>
+ Include dependency graph for structured_trace_util.cpp:

Go to the source code of this file.

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...
 
std::optional< default_trace_steptdefault_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.cpp.

Function Documentation

◆ default_step()

std::optional<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
instructionThe 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_typeThe 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.