structured_trace_util.h

Go to the documentation of this file.

/*******************************************************************\
 
Author: Diffblue
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
#define CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
 
#include "goto_program.h"
#include <string>
class goto_trace_stept;
 
enum class default_step_kindt
{
  LOCATION_ONLY,
  LOOP_HEAD
};
 
default_step_kindt
default_step_kind(const goto_programt::instructiont &instruction);
 
std::string default_step_name(const default_step_kindt &step_type);
 
struct default_trace_stept
{
  default_step_kindt kind;
  bool hidden;
  unsigned thread_number;
  std::size_t step_number;
  source_locationt location;
};
 
optionalt<default_trace_stept> default_step(
  const goto_trace_stept &step,
  const source_locationt &previous_source_location);
 
#endif // CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H