cprover
|
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>
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) |
Traces of GOTO Programs.
Definition in file goto_trace.h.
#define HELP_GOTO_TRACE |
Definition at line 252 of file goto_trace.h.
Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().
#define OPT_GOTO_TRACE |
Definition at line 247 of file goto_trace.h.
#define PARSE_OPTIONS_GOTO_TRACE | ( | cmdline, | |
options | |||
) |
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().
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().
void show_goto_trace | ( | std::ostream & | out, |
const namespacet & | , | ||
const goto_tracet & | , | ||
const trace_optionst & | |||
) |
Definition at line 288 of file goto_trace.cpp.
References goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, goto_trace_stept::CONSTRAINT, goto_trace_stept::DEAD, goto_trace_stept::DECL, from_expr(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, goto_trace_stept::GOTO, id2string(), goto_trace_stept::INPUT, is_index_member_symbol(), goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, goto_trace_stept::OUTPUT, printf_formattert::print(), goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, trace_optionst::show_function_calls, show_state_header(), goto_trace_stept::SPAWN, goto_tracet::steps, trace_numeric_value(), trace_value(), and UNREACHABLE.
Referenced by bmct::error_trace(), bmc_all_propertiest::report(), clobber_parse_optionst::show_counterexample(), and show_goto_trace().
void trace_value | ( | std::ostream & | out, |
const namespacet & | , | ||
const ssa_exprt & | lhs_object, | ||
const exprt & | full_lhs, | ||
const exprt & | value | ||
) |