cprover
structured_trace_util.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Author: Diffblue
4
5\*******************************************************************/
6
10
11#ifndef CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
12#define CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
13
14#include "goto_program.h"
15#include <string>
17
21{
24};
25
34
38std::string default_step_name(const default_step_kindt &step_type);
39
41{
43 bool hidden;
44 unsigned thread_number;
45 std::size_t step_number;
47};
48
50 const goto_trace_stept &step,
51 const source_locationt &previous_source_location);
52
53#endif // CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
Concrete Goto Program.
nonstd::optional< T > optionalt
Definition: optional.h:35
default_step_kindt kind
source_locationt location
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.
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.
default_step_kindt
There are two kinds of step for location markers - location-only and loop-head (for locations associa...
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)