CBMC
structured_trace_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Author: Diffblue
4 
5 \*******************************************************************/
6 
10 
11 #include "structured_trace_util.h"
12 #include "goto_trace.h"
13 
14 #include <algorithm>
15 
18 {
19  const bool is_loophead = std::any_of(
20  instruction.incoming_edges.begin(),
21  instruction.incoming_edges.end(),
22  [](goto_programt::targett t) { return t->is_backwards_goto(); });
23 
24  return is_loophead ? default_step_kindt::LOOP_HEAD
26 }
27 std::string default_step_name(const default_step_kindt &step_type)
28 {
29  switch(step_type)
30  {
32  return "location-only";
34  return "loop-head";
35  }
37 }
38 
39 std::optional<default_trace_stept> default_step(
40  const goto_trace_stept &step,
41  const source_locationt &previous_source_location)
42 {
43  const source_locationt &source_location = step.pc->source_location();
44  if(source_location.is_nil() || source_location.get_file().empty())
45  return {};
46 
47  const auto default_step_kind = ::default_step_kind(*step.pc);
48 
49  // If this is just a source location then we output only the first
50  // location of a sequence of same locations.
51  // However, we don't want to suppress loop head locations because
52  // they might come from different loop iterations. If we suppressed
53  // them it would be impossible to know which loop iteration
54  // we are in.
55  if(
56  source_location == previous_source_location &&
58  {
59  return {};
60  }
61 
63  step.hidden,
64  step.thread_nr,
65  step.step_nr,
66  source_location};
67 }
bool empty() const
Definition: dstring.h:89
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
std::set< targett, target_less_than > incoming_edges
Definition: goto_program.h:450
instructionst::iterator targett
Definition: goto_program.h:614
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
goto_programt::const_targett pc
Definition: goto_trace.h:112
unsigned thread_nr
Definition: goto_trace.h:115
std::size_t step_nr
Number of the step in the trace.
Definition: goto_trace.h:53
bool is_nil() const
Definition: irep.h:368
const irep_idt & get_file() const
Traces of GOTO Programs.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
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.
std::optional< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Utilities for printing location info steps in the trace in a format agnostic way.
default_step_kindt
There are two kinds of step for location markers - location-only and loop-head (for locations associa...