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

std::string trace_value_binary (const exprt &expr, const namespacet &ns)
 
void trace_value (std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
 
void show_state_header (std::ostream &out, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr)
 
bool is_index_member_symbol (const exprt &src)
 
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 235 of file goto_trace.cpp.

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

Referenced by show_goto_trace().

◆ show_goto_trace()

◆ show_state_header()

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

Definition at line 217 of file goto_trace.cpp.

References goto_trace_stept::thread_nr.

Referenced by show_goto_trace().

◆ trace_value()

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

◆ trace_value_binary()

std::string trace_value_binary ( const exprt expr,
const namespacet ns 
)