12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H 41 unsigned atomic_section_id,
48 unsigned atomic_section_id,
55 const exprt &ssa_full_lhs,
56 const exprt &original_full_lhs,
96 const std::list<exprt> &args);
104 const std::list<exprt> &args);
111 const std::list<exprt> &args);
123 const std::string &msg,
135 const std::string &msg,
151 unsigned atomic_section_id,
155 unsigned atomic_section_id,
260 std::ostream &out)
const;
266 for(SSA_stepst::const_iterator
277 for(SSA_stepst::const_iterator
290 SSA_stepst::iterator it=
SSA_steps.begin();
299 void output(std::ostream &out)
const;
308 for(SSA_stepst::const_iterator it=
SSA_steps.begin();
311 if(it->source.thread_nr!=0)
326 const symex_target_equationt::SSA_stepst::const_iterator a,
327 const symex_target_equationt::SSA_stepst::const_iterator b)
339 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H const irept & get_nil_irep()
The type of an expression.
virtual void spawn(const exprt &guard, const sourcet &source)
spawn a new thread
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
virtual void memory_barrier(const exprt &guard, const sourcet &source)
void convert(prop_convt &prop_conv)
unsigned atomic_section_id
bool is_atomic_end() const
bool is_function_return() const
exprt make_expression() const
void convert_assumptions(prop_convt &prop_conv)
converts assumptions
bool is_shared_read() const
Generate Equation using Symbolic Execution.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
just record input
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
record a goto instruction
bool is_constraint() const
bool is_function_call() const
assignment_typet assignment_type
std::list< exprt > converted_io_args
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
start an atomic section
bool is_atomic_begin() const
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
end an atomic section
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
write to a sharedvariable
bool is_shared_write() const
unsigned count_ignored_SSA_steps() const
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
record a constraint
symex_target_equationt(const namespacet &_ns)
void convert_constraints(decision_proceduret &decision_procedure) const
converts constraints
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
declare a fresh variable
virtual ~symex_target_equationt()
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)
write to a variable
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
just record formatted output
bool is_assignment() const
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
just record output
std::list< exprt > io_args
SSA_stepst::iterator get_SSA_step(unsigned s)
void convert_goto_instructions(prop_convt &prop_conv)
converts goto instructions
literalt const_literal(bool value)
bool is_memory_barrier() const
void convert_assignments(decision_proceduret &decision_procedure) const
converts assignments
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
read from a shared variable
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
record an assertion
void convert_assertions(prop_convt &prop_conv)
converts assertions
std::list< SSA_stept > SSA_stepst
void convert_decls(prop_convt &prop_conv) const
converts declarations
Base class for all expressions.
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
virtual void location(const exprt &guard, const sourcet &source)
just record a location
void output(const namespacet &ns, std::ostream &out) const
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
declare a fresh variable
std::ostream & operator<<(std::ostream &out, const symex_target_equationt::SSA_stept &step)
void merge_ireps(SSA_stept &SSA_step)
goto_trace_stept::typet type
unsigned count_assertions() const
Expression providing an SSA-renamed symbol of expressions.
void convert_guards(prop_convt &prop_conv)
converts guards
void convert_io(decision_proceduret &decision_procedure)
converts I/O