CBMC
goto_trace.h File Reference

Traces of GOTO Programs. More...

#include <iosfwd>
#include <vector>
#include <util/message.h>
#include <util/options.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
 Step of the trace of a GOTO program. More...
 
class  goto_tracet
 Trace of a GOTO program. More...
 
struct  trace_optionst
 Options for printing the trace using show_goto_trace. More...
 

Macros

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

Functions

void show_goto_trace (messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &trace_options=trace_optionst::default_options)
 Output the trace on the given stream out. More...
 

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.h.

Macro Definition Documentation

◆ HELP_GOTO_TRACE

#define HELP_GOTO_TRACE
Value:
" {y--trace-json-extended} \t add rawLhs property to trace\n" \
" {y--trace-show-function-calls} \t show function calls in plain trace\n" \
" {y--trace-show-code} \t show original code in plain trace\n" \
" {y--trace-hex} \t represent plain trace values in hex\n" \
" {y--compact-trace} \t give a compact trace\n" \
" {y--stack-trace} \t give a stack trace only\n"

Definition at line 279 of file goto_trace.h.

◆ OPT_GOTO_TRACE

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

Definition at line 271 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); \
if(cmdline.isset("compact-trace")) \
options.set_option("compact-trace", true); \
if(cmdline.isset("stack-trace")) \
options.set_option("stack-trace", true);

Definition at line 287 of file goto_trace.h.

Function Documentation

◆ show_goto_trace()

void show_goto_trace ( messaget::mstreamt out,
const namespacet ns,
const goto_tracet goto_trace,
const trace_optionst trace_options = trace_optionst::default_options 
)

Output the trace on the given stream out.

Definition at line 788 of file goto_trace.cpp.