CBMC
|
Traces of GOTO Programs. More...
#include "goto_trace.h"
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/format_expr.h>
#include <util/merge_irep.h>
#include <util/namespace.h>
#include <util/range.h>
#include <util/string_utils.h>
#include <util/symbol.h>
#include <ansi-c/printf_formatter.h>
#include <langapi/language_util.h>
#include <ostream>
Go to the source code of this file.
Functions | |
static std::optional< symbol_exprt > | get_object_rec (const exprt &src) |
static std::string | numeric_representation (const constant_exprt &expr, const namespacet &ns, 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) |
static void | trace_value (messaget::mstreamt &out, const namespacet &ns, const std::optional< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options) |
static std::string | state_location (const goto_trace_stept &state, const namespacet &ns) |
void | show_state_header (messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options) |
bool | is_index_member_symbol (const exprt &src) |
void | show_compact_goto_trace (messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options) |
show a compact variant of the goto trace on the console More... | |
void | show_full_goto_trace (messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options) |
static void | show_goto_stack_trace (messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace) |
void | show_goto_trace (messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options) |
Output the trace on the given stream out . More... | |
Traces of GOTO Programs.
Definition in file goto_trace.cpp.
|
static |
Definition at line 32 of file goto_trace.cpp.
bool is_index_member_symbol | ( | const exprt & | src | ) |
Definition at line 376 of file goto_trace.cpp.
|
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 |
ns | namespace for symbol type lookups |
options | configuration options |
Definition at line 162 of file goto_trace.cpp.
void show_compact_goto_trace | ( | messaget::mstreamt & | out, |
const namespacet & | ns, | ||
const goto_tracet & | goto_trace, | ||
const trace_optionst & | options | ||
) |
show a compact variant of the goto trace on the console
out | the output stream |
ns | the namespace |
goto_trace | the trace to be shown |
options | any options, e.g., numerical representation |
Definition at line 393 of file goto_trace.cpp.
void show_full_goto_trace | ( | messaget::mstreamt & | out, |
const namespacet & | ns, | ||
const goto_tracet & | goto_trace, | ||
const trace_optionst & | options | ||
) |
Definition at line 515 of file goto_trace.cpp.
|
static |
Definition at line 713 of file goto_trace.cpp.
void show_goto_trace | ( | messaget::mstreamt & | out, |
const namespacet & | ns, | ||
const goto_tracet & | goto_trace, | ||
const trace_optionst & | options | ||
) |
Output the trace on the given stream out
.
Definition at line 788 of file goto_trace.cpp.
void show_state_header | ( | messaget::mstreamt & | out, |
const namespacet & | ns, | ||
const goto_trace_stept & | state, | ||
unsigned | step_nr, | ||
const trace_optionst & | options | ||
) |
Definition at line 352 of file goto_trace.cpp.
|
static |
Definition at line 321 of file goto_trace.cpp.
std::string trace_numeric_value | ( | const exprt & | expr, |
const namespacet & | ns, | ||
const trace_optionst & | options | ||
) |
Definition at line 208 of file goto_trace.cpp.
|
static |
Definition at line 291 of file goto_trace.cpp.