CBMC
structured_trace_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Author: 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>
16 class goto_trace_stept;
17 
21 {
23  LOOP_HEAD
24 };
25 
34 
38 std::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 
49 std::optional<default_trace_stept> default_step(
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:181
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
Concrete Goto Program.
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...
std::optional< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)