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());
207 const exprt &full_lhs,
229 #define OPT_GOTO_TRACE "(trace-json-extended)" 231 #define HELP_GOTO_TRACE \ 232 " --trace-json-extended add rawLhs property to trace\n" 234 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \ 235 if(cmdline.isset("trace-json-extended")) \ 236 options.set_option("trace-json-extended", true); 239 #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
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