cprover
|
#include <symex_target.h>
Classes | |
struct | sourcet |
Public Member Functions | |
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.
|
strong |
Enumerator | |
---|---|
STATE | |
HIDDEN | |
VISIBLE_ACTUAL_PARAMETER | |
HIDDEN_ACTUAL_PARAMETER | |
PHI | |
GUARD |
Definition at line 57 of file symex_target.h.
|
inline |
Definition at line 23 of file symex_target.h.
|
inlinevirtual |
Definition at line 27 of file symex_target.h.
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::vcc().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symex_statet::l2_thread_read_encoding(), goto_symext::phi_function(), goto_symext::symex_assign_symbol(), and goto_symext::symex_goto().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_assume(), and goto_symext::symex_step_goto().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_atomic_begin().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_atomic_end().
|
pure virtual |
Implemented in symex_target_equationt.
|
pure virtual |
Implemented in symex_target_equationt.
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_decl().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_function_call_code().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_end_of_function(), and goto_symext::symex_function_call_code().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_goto().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_input().
Implemented in symex_target_equationt.
Referenced by goto_symext::return_assignment(), goto_symext::symex_function_call_symbol(), goto_symext::symex_goto(), and goto_symext::symex_step().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_other().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_output(), and goto_symext::symex_trace().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_printf().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symex_statet::l2_thread_read_encoding(), and goto_symext::symex_atomic_end().
|
pure virtual |
Implemented in symex_target_equationt.
Referenced by goto_symex_statet::l2_thread_write_encoding(), goto_symext::symex_atomic_end(), and goto_symext::symex_decl().
Implemented in symex_target_equationt.
Referenced by goto_symext::symex_start_thread().