cprover
goto_trace.h File Reference

Traces of GOTO Programs. More...

#include <iosfwd>
#include <vector>
#include <util/namespace.h>
#include <util/options.h>
#include <util/ssa_expr.h>
#include <goto-programs/goto_program.h>
Include dependency graph for goto_trace.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  goto_trace_stept
 TO_BE_DOCUMENTED. More...
 
class  goto_tracet
 TO_BE_DOCUMENTED. More...
 
struct  trace_optionst
 

Macros

#define OPT_GOTO_TRACE
 
#define HELP_GOTO_TRACE
 
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
 

Functions

void show_goto_trace (std::ostream &out, const namespacet &, const goto_tracet &)
 
void show_goto_trace (std::ostream &out, const namespacet &, const goto_tracet &, const trace_optionst &)
 
void trace_value (std::ostream &out, const namespacet &, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
 

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.h.

Macro Definition Documentation

◆ HELP_GOTO_TRACE

#define HELP_GOTO_TRACE
Value:
" --trace-json-extended add rawLhs property to trace\n" \
" --trace-show-function-calls show function calls in plain trace\n" \
" --trace-show-code show original code in plain trace\n" \
" --trace-hex represent plain trace values in hex\n"

Definition at line 252 of file goto_trace.h.

Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().

◆ OPT_GOTO_TRACE

#define OPT_GOTO_TRACE
Value:
"(trace-json-extended)" \
"(trace-show-function-calls)" \
"(trace-show-code)" \
"(trace-hex)"

Definition at line 247 of file goto_trace.h.

◆ PARSE_OPTIONS_GOTO_TRACE

#define PARSE_OPTIONS_GOTO_TRACE (   cmdline,
  options 
)
Value:
if(cmdline.isset("trace-json-extended")) \
options.set_option("trace-json-extended", true); \
if(cmdline.isset("trace-show-function-calls")) \
options.set_option("trace-show-function-calls", true); \
if(cmdline.isset("trace-show-code")) \
options.set_option("trace-show-code", true); \
if(cmdline.isset("trace-hex")) \
options.set_option("trace-hex", true);

Definition at line 258 of file goto_trace.h.

Referenced by cbmc_parse_optionst::get_command_line_options(), and jbmc_parse_optionst::get_command_line_options().

Function Documentation

◆ show_goto_trace() [1/2]

void show_goto_trace ( std::ostream &  out,
const namespacet ,
const goto_tracet  
)

Definition at line 472 of file goto_trace.cpp.

References trace_optionst::default_options, and show_goto_trace().

◆ show_goto_trace() [2/2]

◆ trace_value()

void trace_value ( std::ostream &  out,
const namespacet ,
const ssa_exprt lhs_object,
const exprt full_lhs,
const exprt value 
)