structured_trace_util.h File Reference

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

#include "goto_program.h"
#include <string>

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 class	default_step_kindt { LOCATION_ONLY , 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...
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.h.

Enumeration Type Documentation

default_step_kindt

enum 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()

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.