Go to the documentation of this file.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
optionalt< symbol_exprt > get_lhs_object() const
void show_goto_trace(messaget::mstreamt &out, const namespacet &, const goto_tracet &)
void trim_after(stepst::iterator s)
bool is_memory_barrier() const
The type of an expression, extends irept.
bool is_shared_write() const
Base class for all expressions.
bool is_atomic_begin() const
bool is_function_call() const
bool is_assignment() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool is_function_return() const
void trace_value(messaget::mstreamt &out, const namespacet &, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &)
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
std::vector< exprt > function_arguments
goto_programt::const_targett pc
std::list< exprt > io_argst
bool is_shared_read() const
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
bool is_atomic_end() const
nonstd::optional< T > optionalt
trace_optionst(const optionst &options)
assignment_typet assignment_type
static const trace_optionst default_options
bool get_bool_option(const std::string &option) const
instructionst::const_iterator const_targett
void swap(goto_tracet &other)
goto_trace_stept & get_last_step()
bool is_constraint() const
std::list< goto_trace_stept > stepst
void add_step(const goto_trace_stept &step)