cprover
goto_trace.cpp File Reference

Traces of GOTO Programs. More...

#include "goto_trace.h"
#include <cassert>
#include <ostream>
#include <util/arith_tools.h>
#include <util/format_expr.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 std::string numeric_representation (const exprt &expr, 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 (std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
 
void show_state_header (std::ostream &out, const namespacet &ns, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr, const trace_optionst &options)
 
bool is_index_member_symbol (const exprt &src)
 
void show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
 
void show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
 

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.cpp.

Function Documentation

◆ is_index_member_symbol()

bool is_index_member_symbol ( const exprt src)

Definition at line 276 of file goto_trace.cpp.

References irept::id(), and exprt::op0().

Referenced by show_goto_trace().

◆ numeric_representation()

static std::string numeric_representation ( const exprt expr,
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
optionsconfiguration options
Returns
a string with the numeric representation

Definition at line 115 of file goto_trace.cpp.

References trace_optionst::base_prefix, binary2integer(), irept::get_string(), trace_optionst::hex_representation, id2string(), integer2string(), size_type(), and to_constant_expr().

Referenced by trace_numeric_value().

◆ show_goto_trace() [1/2]

◆ show_goto_trace() [2/2]

void show_goto_trace ( std::ostream &  out,
const namespacet ns,
const goto_tracet goto_trace 
)

Definition at line 472 of file goto_trace.cpp.

References trace_optionst::default_options, and show_goto_trace().

◆ show_state_header()

void show_state_header ( std::ostream &  out,
const namespacet ns,
const goto_trace_stept state,
const source_locationt source_location,
unsigned  step_nr,
const trace_optionst options 
)

◆ trace_numeric_value()

std::string trace_numeric_value ( const exprt expr,
const namespacet ns,
const trace_optionst options 
)

◆ trace_value()

void trace_value ( std::ostream &  out,
const namespacet ns,
const ssa_exprt lhs_object,
const exprt full_lhs,
const exprt value,
const trace_optionst options 
)