cprover
goto_trace.h File Reference

Traces of GOTO Programs. More...

#include <iosfwd>
#include <vector>
#include <util/ssa_expr.h>
#include <goto-programs/goto_program.h>
Include dependency graph for goto_trace.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  goto_trace_stept
 TO_BE_DOCUMENTED. More...
 
class  goto_tracet
 TO_BE_DOCUMENTED. More...
 

Functions

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

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.h.

Function Documentation

§ 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 
)