cprover
|
#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>
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 &) |
Traces of GOTO Programs
Definition in file goto_trace.h.
#define HELP_GOTO_TRACE |
Definition at line 259 of file goto_trace.h.
#define OPT_GOTO_TRACE |
Definition at line 251 of file goto_trace.h.
#define PARSE_OPTIONS_GOTO_TRACE | ( | cmdline, | |
options | |||
) |
Definition at line 267 of file goto_trace.h.
void show_goto_trace | ( | messaget::mstreamt & | out, |
const namespacet & | , | ||
const goto_tracet & | |||
) |
Definition at line 762 of file goto_trace.cpp.
void show_goto_trace | ( | messaget::mstreamt & | out, |
const namespacet & | , | ||
const goto_tracet & | , | ||
const trace_optionst & | |||
) |
Definition at line 748 of file goto_trace.cpp.
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.