12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H 58 pc(_goto_program.instructions.begin()),
86 unsigned atomic_section_id,
87 const sourcet &source) = 0;
99 unsigned atomic_section_id,
100 const sourcet &source) = 0;
116 const exprt &ssa_full_lhs,
117 const exprt &original_full_lhs,
118 const exprt &ssa_rhs,
119 const sourcet &source,
132 const sourcet &source,
143 const sourcet &source)=0;
154 const irep_idt &function_identifier,
155 const std::vector<exprt> &ssa_function_arguments,
156 const sourcet &source,
173 const sourcet &source)=0;
183 const sourcet &source,
185 const std::list<exprt> &args)=0;
196 const sourcet &source,
199 const std::list<exprt> &args)=0;
209 const sourcet &source,
211 const std::list<exprt> &args)=0;
221 const sourcet &source)=0;
232 const std::string &msg,
233 const sourcet &source)=0;
243 const sourcet &source)=0;
252 const std::string &msg,
253 const sourcet &source)=0;
261 const sourcet &source)=0;
269 const sourcet &source)=0;
278 unsigned atomic_section_id,
279 const sourcet &source)=0;
288 unsigned atomic_section_id,
289 const sourcet &source)=0;
301 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H virtual void location(const exprt &guard, const sourcet &source)=0
Record a location.
goto_programt::const_targett pc
virtual void function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)=0
Record a function call.
sourcet(const irep_idt &_function, goto_programt::const_targett _pc)
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
Remove a variable from the scope.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)=0
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignme...
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record ending an atomic section.
sourcet(const irep_idt &_function, const goto_programt &_goto_program)
Identifies source in the context of symbolic execution.
virtual void spawn(const exprt &guard, const sourcet &source)=0
Record spawning a new thread.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)=0
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
The interface of the target container for symbolic execution to record its symbolic steps into.
instructionst::const_iterator const_targett
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
Record an assertion.
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
Base class comparison operator for symbolic execution targets.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)=0
Record a goto instruction.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
Record an assumption.
A generic container class for the GOTO intermediate representation of one function.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
Write to a local variable.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record a beginning of an atomic section.
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)=0
Record formatted output.
Base class for all expressions.
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)=0
Record return from a function.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
Record an output.
Expression to hold a symbol (variable)
Expression providing an SSA-renamed symbol of expressions.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)=0
Record a global constraint: there is no guard limiting its scope.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
Declare a fresh variable.
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
Record creating a memory barrier.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
Record an input.