Loading...

Searching...

No Matches

goto_trace.cpp File Reference

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 dependency graph for goto_trace.cpp:

[フレーム]

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.

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, std::size_t 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

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.

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.cpp.

Function Documentation

◆ get_object_rec()

static std::optional< symbol_exprt > get_object_rec ( const exprt & src )

static

Definition at line 30 of file goto_trace.cpp.

◆ is_index_member_symbol()

bool is_index_member_symbol ( const exprt & src )

Definition at line 374 of file goto_trace.cpp.

◆ numeric_representation()

static std::string numeric_representation ( const constant_exprt & expr,

const namespacet & ns,

const trace_optionst & options

)

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 160 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 391 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 513 of file goto_trace.cpp.

◆ show_goto_stack_trace()

static void show_goto_stack_trace ( messaget::mstreamt & out,

const namespacet & ns,

const goto_tracet & goto_trace

)

static

Definition at line 711 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 786 of file goto_trace.cpp.

◆ show_state_header()

void show_state_header ( messaget::mstreamt & out,

const namespacet & ns,

const goto_trace_stept & state,

std::size_t step_nr,

const trace_optionst & options

)

Definition at line 350 of file goto_trace.cpp.

◆ state_location()

static std::string state_location ( const goto_trace_stept & state,

const namespacet & ns

)

static

Definition at line 319 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 206 of file goto_trace.cpp.

◆ trace_value()

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

Definition at line 289 of file goto_trace.cpp.