14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H 15 #define CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H 124 std::ostream &out)
const;
149 typedef std::list<goto_trace_stept>
stepst;
164 std::ostream &out)
const;
174 steps.push_back(step);
180 assert(s!=
steps.end());
194 const exprt &full_lhs,
197 #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
void trace_value(std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
void swap(goto_tracet &other)
bool is_shared_read() const
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
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
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.
bool is_constraint() const
bool is_memory_barrier() const
bool is_assignment() const
Expression providing an SSA-renamed symbol of expressions.
assignment_typet assignment_type