cprover
goto_trace.h File Reference

Traces of GOTO Programs. More...

#include <iosfwd>
#include <vector>
#include <util/message.h>
#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
 
#define HELP_GOTO_TRACE
 
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
 

Functions

void show_goto_trace (messaget::mstreamt &out, const namespacet &, const goto_tracet &)
 
void show_goto_trace (messaget::mstreamt &out, const namespacet &, const goto_tracet &, const trace_optionst &)
 
void trace_value (messaget::mstreamt &out, const namespacet &, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &)
 

Detailed Description

Traces of GOTO Programs.

Definition in file goto_trace.h.

Macro Definition Documentation

◆ HELP_GOTO_TRACE

#define HELP_GOTO_TRACE
Value:
" --trace-json-extended add rawLhs property to trace\n" \
" --trace-show-function-calls show function calls in plain trace\n" \
" --trace-show-code show original code in plain trace\n" \
" --trace-hex represent plain trace values in hex\n" \
" --compact-trace give a compact trace\n" \
" --stack-trace give a stack trace only\n"

Definition at line 259 of file goto_trace.h.

◆ OPT_GOTO_TRACE

#define OPT_GOTO_TRACE
Value:
"(trace-json-extended)" \
"(trace-show-function-calls)" \
"(trace-show-code)" \
"(trace-hex)" \
"(compact-trace)" \
"(stack-trace)"

Definition at line 251 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); \
if(cmdline.isset("trace-show-function-calls")) \
options.set_option("trace-show-function-calls", true); \
if(cmdline.isset("trace-show-code")) \
options.set_option("trace-show-code", true); \
if(cmdline.isset("trace-hex")) \
options.set_option("trace-hex", true); \
if(cmdline.isset("compact-trace")) \
options.set_option("compact-trace", true); \
if(cmdline.isset("stack-trace")) \
options.set_option("stack-trace", true);

Definition at line 267 of file goto_trace.h.

Function Documentation

◆ show_goto_trace() [1/2]

void show_goto_trace ( messaget::mstreamt out,
const namespacet ,
const goto_tracet  
)

Definition at line 762 of file goto_trace.cpp.

◆ show_goto_trace() [2/2]

void show_goto_trace ( messaget::mstreamt out,
const namespacet ,
const goto_tracet ,
const trace_optionst  
)

Definition at line 748 of file goto_trace.cpp.

◆ trace_value()

void trace_value ( messaget::mstreamt out,
const namespacet ,
const optionalt< symbol_exprt > &  lhs_object,
const exprt full_lhs,
const exprt value,
const trace_optionst  
)

Definition at line 256 of file goto_trace.cpp.