14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H 15 #define CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H 129 std::ostream &out)
const;
153 typedef std::list<goto_trace_stept>
stepst;
168 std::ostream &out)
const;
178 steps.push_back(step);
247 const exprt &full_lhs,
251 #define OPT_GOTO_TRACE \ 252 "(trace-json-extended)" \ 253 "(trace-show-function-calls)" \ 254 "(trace-show-code)" \ 259 #define HELP_GOTO_TRACE \ 260 " --trace-json-extended add rawLhs property to trace\n" \ 261 " --trace-show-function-calls show function calls in plain trace\n" \ 262 " --trace-show-code show original code in plain trace\n" \ 263 " --trace-hex represent plain trace values in hex\n" \ 264 " --compact-trace give a compact trace\n" \ 265 " --stack-trace give a stack trace only\n" 267 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \ 268 if(cmdline.isset("trace-json-extended")) \ 269 options.set_option("trace-json-extended", true); \ 270 if(cmdline.isset("trace-show-function-calls")) \ 271 options.set_option("trace-show-function-calls", true); \ 272 if(cmdline.isset("trace-show-code")) \ 273 options.set_option("trace-show-code", true); \ 274 if(cmdline.isset("trace-hex")) \ 275 options.set_option("trace-hex", true); \ 276 if(cmdline.isset("compact-trace")) \ 277 options.set_option("compact-trace", true); \ 278 if(cmdline.isset("stack-trace")) \ 279 options.set_option("stack-trace", true); 281 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
The type of an expression, extends irept.
bool is_shared_write() const
std::vector< exprt > function_arguments
void trim_after(stepst::iterator s)
std::list< exprt > io_argst
void trace_value(messaget::mstreamt &out, const namespacet &, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &)
std::list< goto_trace_stept > stepst
goto_trace_stept & get_last_step()
void swap(goto_tracet &other)
bool is_shared_read() const
goto_programt::const_targett pc
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
void add_step(const goto_trace_stept &step)
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
bool is_function_call() const
nonstd::optional< T > optionalt
bool get_bool_option(const std::string &option) const
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
bool is_atomic_end() const
optionalt< symbol_exprt > get_lhs_object() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool is_function_return() const
bool is_atomic_begin() const
Base class for all expressions.
trace_optionst(const optionst &options)
bool is_constraint() const
bool is_memory_barrier() const
bool is_assignment() const
static const trace_optionst default_options
void show_goto_trace(messaget::mstreamt &out, const namespacet &, const goto_tracet &)
assignment_typet assignment_type