Go to the documentation of this file.
23 "we don't support nesting of atomic sections",
43 "ATOMIC_END unmatched", state.
source.
pc->source_location);
51 r.set_level_2(pair.second.first);
55 guardt read_guard(pair.second.second.front());
56 for(std::list<guardt>::const_iterator it = ++(pair.second.second.begin());
57 it != pair.second.second.end();
77 guardt write_guard(pair.second.front());
78 for(std::list<guardt>::const_iterator it = ++(pair.second.begin());
79 it != pair.second.end();
#define PRECONDITION(CONDITION)
virtual void symex_atomic_begin(statet &)
goto_programt::const_targett pc
symex_target_equationt & target
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
Base class for all expressions.
symex_targett::sourcet source
virtual void do_simplify(exprt &)
bool is_false() const
Return whether the expression is a constant representing false.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
Expression providing an SSA-renamed symbol of expressions.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
unsigned atomic_section_id
const irep_idt & get_identifier() const
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
unsigned atomic_section_counter
virtual void symex_atomic_end(statet &)
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
void set_level_2(unsigned i)