12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H 51 pc(_goto_program.instructions.begin()),
71 unsigned atomic_section_id,
72 const sourcet &source)=0;
78 unsigned atomic_section_id,
79 const sourcet &source)=0;
85 const exprt &ssa_full_lhs,
86 const exprt &original_full_lhs,
88 const sourcet &source,
95 const sourcet &source,
102 const sourcet &source)=0;
108 const sourcet &source)=0;
114 const sourcet &source)=0;
119 const sourcet &source)=0;
124 const sourcet &source,
126 const std::list<exprt> &args)=0;
131 const sourcet &source,
134 const std::list<exprt> &args)=0;
139 const sourcet &source,
141 const std::list<exprt> &args)=0;
147 const sourcet &source)=0;
153 const std::string &msg,
154 const sourcet &source)=0;
160 const sourcet &source)=0;
165 const std::string &msg,
166 const sourcet &source)=0;
171 const sourcet &source)=0;
176 const sourcet &source)=0;
181 unsigned atomic_section_id,
182 const sourcet &source)=0;
185 unsigned atomic_section_id,
186 const sourcet &source)=0;
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
virtual void spawn(const exprt &guard, const sourcet &source)=0
instructionst::const_iterator const_targett
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
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
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
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
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