31 data_typet::const_iterator it;
33 for(it=
data.cbegin(); it!=
data.cend(); ++it)
87 if(
it1->id !=
e1.variable)
92 if(
it1->id!=
e1.variable ||
it1->loc!=
e1.source_location)
100 if(
it2->id!=
e2.variable)
105 if(
it2->id!=
e2.variable ||
it2->loc!=
e2.source_location)
109 if(
it1->eq_class==
it2->eq_class)
167 data_typet::const_iterator it;
168 std::map<unsigned, std::set<source_locationt> >
classed;
170 for(it=
data.cbegin(); it!=
data.cend(); ++it)
174 std::set<source_locationt> s;
179 classed[it->eq_class].insert(it->loc);
182 for(std::map<
unsigned, std::set<source_locationt> >::const_iterator
187 std::set<source_locationt>::const_iterator
l_it;
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'.
int __CPROVER_ID java::java io InputStream read
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
ssize_t write(int fildes, const void *buf, size_t nbyte)