cprover
|
Traces of GOTO Programs. More...
#include <iosfwd>
#include <vector>
#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... | |
Functions | |
void | show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace) |
void | trace_value (std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value) |
Traces of GOTO Programs.
Definition in file goto_trace.h.
void show_goto_trace | ( | std::ostream & | out, |
const namespacet & | ns, | ||
const goto_tracet & | goto_trace | ||
) |
Definition at line 239 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, show_state_header(), goto_trace_stept::SPAWN, goto_tracet::steps, trace_value(), and trace_value_binary().
Referenced by bmct::error_trace(), bmc_all_propertiest::report(), bmc_covert::satisfying_assignment(), clobber_parse_optionst::show_counterexample(), symex_parse_optionst::show_counterexample(), and goto_tracet::trim_after().
void trace_value | ( | std::ostream & | out, |
const namespacet & | ns, | ||
const ssa_exprt & | lhs_object, | ||
const exprt & | full_lhs, | ||
const exprt & | value | ||
) |
Definition at line 179 of file goto_trace.cpp.
References from_expr(), ssa_exprt::get_object_name(), irept::is_nil(), irept::is_not_nil(), and trace_value_binary().
Referenced by show_goto_trace(), and goto_tracet::trim_after().