27 data_typet::const_iterator it;
29 for(it=
data.cbegin(); it!=
data.cend(); ++it)
83 if(
it1->id !=
e1.variable)
88 if(
it1->id!=
e1.variable ||
it1->loc!=
e1.source_location)
96 if(
it2->id!=
e2.variable)
101 if(
it2->id!=
e2.variable ||
it2->loc!=
e2.source_location)
105 if(
it1->eq_class==
it2->eq_class)
150 if(
it3->eq_class==from)
163 data_typet::const_iterator it;
164 std::map<unsigned, std::set<source_locationt> >
classed;
166 for(it=
data.cbegin(); it!=
data.cend(); ++it)
170 std::set<source_locationt> s;
175 classed[it->eq_class].insert(it->loc);
178 for(std::map<
unsigned, std::set<source_locationt> >::const_iterator
183 std::set<source_locationt>::const_iterator
l_it;
source_locationt source_location
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void dp_merge()
merge in N^3
void print(messaget &message)
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write)
Class that provides messages with a built-in verbosity 'level'.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.