12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H 51 pc(_goto_program.instructions.begin()),
61 VISIBLE_ACTUAL_PARAMETER,
62 HIDDEN_ACTUAL_PARAMETER,
71 unsigned atomic_section_id,
78 unsigned atomic_section_id,
85 const exprt &ssa_full_lhs,
86 const exprt &original_full_lhs,
126 const std::list<exprt> &args)=0;
134 const std::list<exprt> &args)=0;
141 const std::list<exprt> &args)=0;
153 const std::string &msg,
165 const std::string &msg,
181 unsigned atomic_section_id,
185 unsigned atomic_section_id,
193 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H sourcet(goto_programt::const_targett _pc)
virtual void location(const exprt &guard, const sourcet &source)=0
goto_programt::const_targett pc
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
sourcet(const goto_programt &_goto_program)
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
instructionst::const_iterator const_targett
virtual void spawn(const exprt &guard, const sourcet &source)=0
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)=0
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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 atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=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
Base class for all expressions.
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
Expression to hold a symbol (variable)
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
Expression providing an SSA-renamed symbol of expressions.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)=0
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0