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...
class	goto_trace_constant_pointer_exprt
	Variety of constant expression only used in the context of a GOTO trace, to give both the numeric value and the symbolic value of a pointer, e.g. 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.
template<>
bool	can_cast_expr< goto_trace_constant_pointer_exprt > (const exprt &base)
const goto_trace_constant_pointer_exprt &	to_goto_trace_constant_pointer_expr (const exprt &expr)

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 277 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 269 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 285 of file goto_trace.h.

Function Documentation

can_cast_expr< goto_trace_constant_pointer_exprt >()

template<>

bool can_cast_expr< goto_trace_constant_pointer_exprt > ( const exprt &  base )

inline

Definition at line 315 of file goto_trace.h.

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 785 of file goto_trace.cpp.

to_goto_trace_constant_pointer_expr()

const goto_trace_constant_pointer_exprt & to_goto_trace_constant_pointer_expr ( const exprt &  expr )

inline

Definition at line 321 of file goto_trace.h.