CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
39
48
49std::optional<default_trace_stept> default_step(
50 const goto_trace_stept &step,
52
53#endif // CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
This class represents an instruction in the GOTO intermediate representation.
Step of the trace of a GOTO program.
Definition goto_trace.h:50
Concrete Goto Program.
default_step_kindt 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.
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)