21 throw "nested atomic section detected at "+
22 state.
source.
pc->source_location.as_string();
40 throw "ATOMIC_END unmatched";
45 for(goto_symex_statet::read_in_atomic_sectiont::const_iterator
54 assert(!r_it->second.second.empty());
55 guardt read_guard(r_it->second.second.front());
56 for(std::list<guardt>::const_iterator
57 it=++(r_it->second.second.begin());
58 it!=r_it->second.second.end();
61 exprt read_guard_expr=read_guard.as_expr();
71 for(goto_symex_statet::written_in_atomic_sectiont::const_iterator
80 assert(!w_it->second.empty());
81 guardt write_guard(w_it->second.front());
82 for(std::list<guardt>::const_iterator
83 it=++(w_it->second.begin());
84 it!=w_it->second.end();
87 exprt write_guard_expr=write_guard.as_expr();
virtual void do_simplify(exprt &expr)
virtual void symex_atomic_begin(statet &state)
goto_programt::const_targett pc
read_in_atomic_sectiont read_in_atomic_section
const irep_idt & get_identifier() const
written_in_atomic_sectiont written_in_atomic_section
void set_level_2(unsigned i)
goto_symex_statet::level2t level2
virtual void atomic_end(const exprt &guard, 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
unsigned atomic_section_id
unsigned atomic_section_counter
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
virtual void symex_atomic_end(statet &state)
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.
symex_targett::sourcet source