#include "goto_trace.h"#include <ostream>#include <util/arith_tools.h>#include <util/byte_operators.h>#include <util/c_types.h>#include <util/format_expr.h>#include <util/merge_irep.h>#include <util/range.h>#include <util/string_utils.h>#include <util/symbol.h>#include <langapi/language_util.h>#include "printf_formatter.h"
Include dependency graph for goto_trace.cpp:Go to the source code of this file.
Functions | |
| static optionalt< 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 optionalt< 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... | |
Detailed Description
Traces of GOTO Programs
Definition in file goto_trace.cpp.
Function Documentation
◆ get_object_rec()
|
static |
Definition at line 31 of file goto_trace.cpp.
◆ is_index_member_symbol()
| bool is_index_member_symbol | ( | const exprt & | src | ) |
Definition at line 375 of file goto_trace.cpp.
◆ numeric_representation()
|
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
- Parameters
-
expr expression to get numeric representation from ns namespace for symbol type lookups options configuration options
- Returns
- a string with the numeric representation
Definition at line 161 of file goto_trace.cpp.
◆ show_compact_goto_trace()
| 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
- Parameters
-
out the output stream ns the namespace goto_trace the trace to be shown options any options, e.g., numerical representation
Definition at line 392 of file goto_trace.cpp.
◆ show_full_goto_trace()
| void show_full_goto_trace | ( | messaget::mstreamt & | out, |
| const namespacet & | ns, | ||
| const goto_tracet & | goto_trace, | ||
| const trace_optionst & | options | ||
| ) |
Definition at line 520 of file goto_trace.cpp.
◆ show_goto_stack_trace()
|
static |
Definition at line 717 of file goto_trace.cpp.
◆ show_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.
Definition at line 792 of file goto_trace.cpp.
◆ show_state_header()
| 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 351 of file goto_trace.cpp.
◆ state_location()
|
static |
Definition at line 320 of file goto_trace.cpp.
◆ trace_numeric_value()
| std::string trace_numeric_value | ( | const exprt & | expr, |
| const namespacet & | ns, | ||
| const trace_optionst & | options | ||
| ) |
Definition at line 207 of file goto_trace.cpp.
◆ trace_value()
|
static |
Definition at line 290 of file goto_trace.cpp.
