|
| symex_targett () |
|
virtual | ~symex_targett () |
|
virtual void | shared_read (const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0 |
|
virtual void | shared_write (const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0 |
|
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 |
|
virtual void | decl (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0 |
|
virtual void | dead (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0 |
|
virtual void | function_call (const exprt &guard, const irep_idt &identifier, const sourcet &source)=0 |
|
virtual void | function_return (const exprt &guard, const irep_idt &identifier, const sourcet &source)=0 |
|
virtual void | location (const exprt &guard, const sourcet &source)=0 |
|
virtual void | output (const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0 |
|
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 |
|
virtual void | input (const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0 |
|
virtual void | assumption (const exprt &guard, const exprt &cond, const sourcet &source)=0 |
|
virtual void | assertion (const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0 |
|
virtual void | goto_instruction (const exprt &guard, const exprt &cond, const sourcet &source)=0 |
|
virtual void | constraint (const exprt &cond, const std::string &msg, const sourcet &source)=0 |
|
virtual void | spawn (const exprt &guard, const sourcet &source)=0 |
|
virtual void | memory_barrier (const exprt &guard, const sourcet &source)=0 |
|
virtual void | atomic_begin (const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0 |
|
virtual void | atomic_end (const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0 |
|
Definition at line 20 of file symex_target.h.