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_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.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

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.