cprover
|
Traces of GOTO Programs. More...
#include "goto_trace.h"
#include <cassert>
#include <ostream>
#include <util/arith_tools.h>
#include <util/symbol.h>
#include <ansi-c/printf_formatter.h>
#include <langapi/language_util.h>
Go to the source code of this file.
Functions | |
std::string | trace_value_binary (const exprt &expr, const namespacet &ns) |
void | trace_value (std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value) |
void | show_state_header (std::ostream &out, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr) |
bool | is_index_member_symbol (const exprt &src) |
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 227 of file goto_trace.cpp.
References irept::id(), and exprt::op0().
Referenced by show_goto_trace().
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(), and symex_parse_optionst::show_counterexample().
void show_state_header | ( | std::ostream & | out, |
const goto_trace_stept & | state, | ||
const source_locationt & | source_location, | ||
unsigned | step_nr | ||
) |
Definition at line 209 of file goto_trace.cpp.
References goto_trace_stept::thread_nr.
Referenced by show_goto_trace().
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().
std::string trace_value_binary | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 116 of file goto_trace.cpp.
References namespace_baset::follow(), forall_operands, irept::get_string(), irept::id(), exprt::is_true(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by show_goto_trace(), and trace_value().