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/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

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 227 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 209 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 
)