31 std::unordered_set<irep_idt> init_done;
32 bool spawn_seen=
false;
36 for(eventst::const_iterator
46 else if(!e_it->is_shared_read() &&
47 !e_it->is_shared_write())
52 if(init_done.find(a)!=init_done.end())
56 e_it->is_shared_read() ||
57 !e_it->guard.is_true())
68 SSA_step.
source=e_it->source;
83 std::map<unsigned, unsigned> counter;
85 for(eventst::const_iterator
90 if(e_it->is_shared_read() ||
91 e_it->is_shared_write() ||
94 unsigned thread_nr=e_it->source.thread_nr;
100 if(e_it->is_shared_read())
101 a_rec.
reads.push_back(e_it);
103 a_rec.
writes.push_back(e_it);
107 unsigned cnt=counter[thread_nr]++;
112 for(address_mapt::const_iterator
117 const a_rect &a_rec=a_it->second;
118 if(a_rec.
reads.empty())
121 statistics() <<
"Shared " << a_it->first <<
": " 122 << a_rec.
reads.size() <<
"R/" 131 if(event->is_shared_write())
133 else if(event->is_shared_read())
148 if(event->is_shared_write())
150 else if(event->is_shared_read())
152 else if(event->is_spawn())
175 const axiomt axiom_bits[]=
184 ops.reserve(
sizeof(axiom_bits)/
sizeof(
axiomt));
186 for(
int i=0; i<int(
sizeof(axiom_bits)/
sizeof(
axiomt)); ++i)
188 const axiomt ax=axiom_bits[i];
193 if(e1->atomic_section_id!=0 &&
194 e1->atomic_section_id==e2->atomic_section_id)
209 const std::string &msg,
Fixed-width bit-vector with unsigned binary interpretation.
irep_idt address(event_it event) const
A base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
unsigned atomic_section_id
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
symbol_exprt clock(event_it e, axiomt axiom)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
exprt before(event_it e1, event_it e2, unsigned axioms)
void build_event_lists(symex_target_equationt &)
#define POSTCONDITION(CONDITION)
Add constraints to equation encoding partial orders on events.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
The Boolean constant true.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
Identifies source in the context of symbolic execution.
void add_init_writes(symex_target_equationt &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
partial_order_concurrencyt(const namespacet &_ns)
std::vector< exprt > operandst
Single SSA step in the equation.
std::list< SSA_stept > SSA_stepst
eventst::const_iterator event_it
Base class for all expressions.
virtual ~partial_order_concurrencyt()
#define UNREACHABLE
This should be used to mark dead code.
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Expression to hold a symbol (variable)
goto_trace_stept::typet type
mstreamt & statistics() const
bool simplify(exprt &expr, const namespacet &ns)