cprover
goto_trace.h File Reference

Traces of GOTO Programs. More...

#include <iosfwd>
#include <vector>
#include <util/namespace.h>
#include <util/options.h>
#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...
 
struct  trace_optionst
 

Macros

#define OPT_GOTO_TRACE   "(trace-json-extended)"
 
#define HELP_GOTO_TRACE   " --trace-json-extended add rawLhs property to trace\n"
 
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
 

Functions

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

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.h.

Macro Definition Documentation

◆ HELP_GOTO_TRACE

#define HELP_GOTO_TRACE   " --trace-json-extended add rawLhs property to trace\n"

Definition at line 231 of file goto_trace.h.

Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().

◆ OPT_GOTO_TRACE

#define OPT_GOTO_TRACE   "(trace-json-extended)"

Definition at line 229 of file goto_trace.h.

◆ PARSE_OPTIONS_GOTO_TRACE

#define PARSE_OPTIONS_GOTO_TRACE (   cmdline,
  options 
)
Value:
if(cmdline.isset("trace-json-extended")) \
options.set_option("trace-json-extended", true);

Definition at line 234 of file goto_trace.h.

Referenced by cbmc_parse_optionst::get_command_line_options(), and jbmc_parse_optionst::get_command_line_options().

Function Documentation

◆ show_goto_trace()

◆ trace_value()

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