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.