14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H 15 #define CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H 129 std::ostream &out)
const;
155 typedef std::list<goto_trace_stept>
stepst;
170 std::ostream &out)
const;
180 steps.push_back(step);
193 assert(s!=
steps.end());
243 const exprt &full_lhs,
247 #define OPT_GOTO_TRACE "(trace-json-extended)" \ 248 "(trace-show-function-calls)" \ 249 "(trace-show-code)" \ 252 #define HELP_GOTO_TRACE \ 253 " --trace-json-extended add rawLhs property to trace\n" \ 254 " --trace-show-function-calls show function calls in plain trace\n" \ 255 " --trace-show-code show original code in plain trace\n" \ 256 " --trace-hex represent plain trace values in hex\n" 258 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \ 259 if(cmdline.isset("trace-json-extended")) \ 260 options.set_option("trace-json-extended", true); \ 261 if(cmdline.isset("trace-show-function-calls")) \ 262 options.set_option("trace-show-function-calls", true); \ 263 if(cmdline.isset("trace-show-code")) \ 264 options.set_option("trace-show-code", true); \ 265 if(cmdline.isset("trace-hex")) \ 266 options.set_option("trace-hex", true); 269 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
The type of an expression.
bool is_shared_write() const
void trim_after(stepst::iterator s)
std::list< exprt > io_argst
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
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)
bool get_bool_option(const std::string &option) const
instructionst::const_iterator const_targett
bool is_atomic_end() 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
Expression providing an SSA-renamed symbol of expressions.
assignment_typet assignment_type