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);
56 for(std::list<guardt>::const_iterator it = ++(
pair.second.second.begin());
57 it !=
pair.second.second.end();
73 w.set_level_2(state.
get_level2().latest_index(
w.get_identifier()));
78 for(std::list<guardt>::const_iterator it = ++(
pair.second.begin());
79 it !=
pair.second.end();
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
unsigned atomic_section_id
Threads.
const symex_level2t & get_level2() const
Central data structure: state.
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
symex_targett::sourcet source
virtual void symex_atomic_begin(statet &state)
Symbolically execute an ATOMIC_BEGIN instruction.
symex_target_equationt & target
The equation that this execution is building up.
unsigned atomic_section_counter
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
virtual void do_simplify(exprt &expr)
virtual void symex_atomic_end(statet &state)
Symbolically execute an ATOMIC_END instruction.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Expression providing an SSA-renamed symbol of expressions.
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...
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of 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 shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
#define PRECONDITION(CONDITION)
goto_programt::const_targett pc