cprover
goto_trace.cpp File Reference
#include "goto_trace.h"
#include <ostream>
#include <util/arith_tools.h>
#include <util/format_expr.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_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)
 
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)
 
void show_goto_trace (messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
 

Detailed Description

Traces of GOTO Programs

Definition in file goto_trace.cpp.

Function Documentation

◆ get_object_rec()

static optionalt<symbol_exprt> get_object_rec ( const exprt src)
static

Definition at line 28 of file goto_trace.cpp.

◆ is_index_member_symbol()

bool is_index_member_symbol ( const exprt src)

Definition at line 341 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 135 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 358 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 479 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 673 of file goto_trace.cpp.

◆ show_goto_trace() [1/2]

void show_goto_trace ( messaget::mstreamt out,
const namespacet ns,
const goto_tracet goto_trace 
)

Definition at line 762 of file goto_trace.cpp.

◆ show_goto_trace() [2/2]

void show_goto_trace ( messaget::mstreamt out,
const namespacet ns,
const goto_tracet goto_trace,
const trace_optionst options 
)

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

◆ state_location()

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

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

◆ trace_value()

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 
)

Definition at line 256 of file goto_trace.cpp.