goto_trace.h File Reference

Traces of GOTO Programs. More...

#include <iosfwd>
#include <vector>
#include <util/message.h>
#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 (messaget::mstreamt &out, const namespacet &, const goto_tracet &)
void	show_goto_trace (messaget::mstreamt &out, const namespacet &, const goto_tracet &, const trace_optionst &)
void	trace_value (messaget::mstreamt &out, const namespacet &, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &)

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"        \
  " --compact-trace              give a compact trace\n"                       \
  " --stack-trace                give a stack trace only\n"

Definition at line 259 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 251 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 267 of file goto_trace.h.

Function Documentation

show_goto_trace() [1/2]

void show_goto_trace	(	messaget::mstreamt &	out,
		const namespacet &	,
		const goto_tracet &
	)

Definition at line 762 of file goto_trace.cpp.

show_goto_trace() [2/2]

void show_goto_trace	(	messaget::mstreamt &	out,
		const namespacet &	,
		const goto_tracet &	,
		const trace_optionst &
	)

Definition at line 748 of file goto_trace.cpp.

trace_value()

void trace_value	(	messaget::mstreamt &	out,
		const namespacet &	,
		const optionalt< symbol_exprt > &	lhs_object,
		const exprt &	full_lhs,
		const exprt &	value,
		const trace_optionst &
	)

Definition at line 256 of file goto_trace.cpp.