CBMC
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 <ostream>
+ Include dependency graph for goto_trace.cpp:

Go to the source code of this file.

Functions

static std::optional< symbol_exprtget_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...
 

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 32 of file goto_trace.cpp.

◆ is_index_member_symbol()

bool is_index_member_symbol ( const exprt src)

Definition at line 376 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
exprexpression to get numeric representation from
nsnamespace for symbol type lookups
optionsconfiguration options
Returns
a string with the numeric representation

Definition at line 162 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
outthe output stream
nsthe namespace
goto_tracethe trace to be shown
optionsany options, e.g., numerical representation

Definition at line 393 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 515 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 713 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 788 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 352 of file goto_trace.cpp.

◆ state_location()

static std::string state_location ( const goto_trace_stept state,
const namespacet ns 
)
static

Definition at line 321 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 208 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 291 of file goto_trace.cpp.