cprover
|
Traces of GOTO Programs. More...
#include "goto_trace.h"
#include <cassert>
#include <ostream>
#include <util/arith_tools.h>
#include <util/format_expr.h>
#include <util/symbol.h>
#include <langapi/language_util.h>
#include "printf_formatter.h"
Go to the source code of this file.
Functions | |
static std::string | numeric_representation (const exprt &expr, const trace_optionst &options) |
Returns the numeric representation of an expression, based on options. More... | |
std::string | trace_numeric_value (const exprt &expr, const namespacet &ns, const trace_optionst &options) |
void | trace_value (std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options) |
void | show_state_header (std::ostream &out, const namespacet &ns, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr, const trace_optionst &options) |
bool | is_index_member_symbol (const exprt &src) |
void | show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options) |
void | show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace) |
Traces of GOTO Programs.
Definition in file goto_trace.cpp.
bool is_index_member_symbol | ( | const exprt & | src | ) |
Definition at line 276 of file goto_trace.cpp.
References irept::id(), and exprt::op0().
Referenced by show_goto_trace().
|
static |
Returns the numeric representation of an expression, based on options.
The default is binary without a base-prefix. Setting options.hex_representation to be true outputs hex format. Setting options.base_prefix to be true appends either 0b or 0x to the number to indicate the base
expr | expression to get numeric representation from |
options | configuration options |
Definition at line 115 of file goto_trace.cpp.
References trace_optionst::base_prefix, binary2integer(), irept::get_string(), trace_optionst::hex_representation, id2string(), integer2string(), size_type(), and to_constant_expr().
Referenced by trace_numeric_value().
void show_goto_trace | ( | std::ostream & | out, |
const namespacet & | ns, | ||
const goto_tracet & | goto_trace, | ||
const trace_optionst & | options | ||
) |
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 show_goto_trace | ( | std::ostream & | out, |
const namespacet & | ns, | ||
const goto_tracet & | goto_trace | ||
) |
Definition at line 472 of file goto_trace.cpp.
References trace_optionst::default_options, and show_goto_trace().
void show_state_header | ( | std::ostream & | out, |
const namespacet & | ns, | ||
const goto_trace_stept & | state, | ||
const source_locationt & | source_location, | ||
unsigned | step_nr, | ||
const trace_optionst & | options | ||
) |
Definition at line 248 of file goto_trace.cpp.
References as_string(), goto_trace_stept::pc, trace_optionst::show_code, and goto_trace_stept::thread_nr.
Referenced by show_goto_trace().
std::string trace_numeric_value | ( | const exprt & | expr, |
const namespacet & | ns, | ||
const trace_optionst & | options | ||
) |
Definition at line 146 of file goto_trace.cpp.
References namespace_baset::follow(), forall_operands, irept::id(), integer2string(), exprt::is_true(), numeric_representation(), exprt::op0(), exprt::operands(), PRECONDITION, to_integer(), and exprt::type().
Referenced by show_goto_trace(), and trace_value().
void trace_value | ( | std::ostream & | out, |
const namespacet & | ns, | ||
const ssa_exprt & | lhs_object, | ||
const exprt & | full_lhs, | ||
const exprt & | value, | ||
const trace_optionst & | options | ||
) |
Definition at line 217 of file goto_trace.cpp.
References from_expr(), ssa_exprt::get_object_name(), irept::is_nil(), irept::is_not_nil(), and trace_numeric_value().
Referenced by show_goto_trace().