31 data_typet::const_iterator it;
33 for(it=
data.cbegin(); it!=
data.cend(); ++it)
35 if(local_read && it->id==
read.id)
45 if(local_write && it->id==
write.id)
78 for(
auto it1=
data.cbegin(); it1!=
data.cend(); ++it1)
96 for(; it2!=
data.cend(); ++it2)
109 if(it1->eq_class==it2->eq_class)
126 unsigned initial_size=
data.size();
132 for(
auto it1=
data.cbegin(); it1!=
data.cend(); ++it1)
140 for(; it2!=
data.cend(); ++it2)
153 for(
auto it3=
data.begin(); it3!=
data.end(); ++it3)
154 if(it3->eq_class==from)
158 INVARIANT(initial_size>
data.size(),
"strictly monotonous => converges");
167 data_typet::const_iterator it;
168 std::map<unsigned, std::set<source_locationt> > classed;
170 for(it=
data.cbegin(); it!=
data.cend(); ++it)
172 if(classed.find(it->eq_class)==classed.end())
174 std::set<source_locationt> s;
176 classed[it->eq_class]=s;
179 classed[it->eq_class].insert(it->loc);
182 for(std::map<
unsigned, std::set<source_locationt> >::const_iterator
183 m_it=classed.begin();
184 m_it!=classed.end(); ++m_it)
187 std::set<source_locationt>::const_iterator l_it;
188 for(l_it=m_it->second.begin(); l_it!=m_it->second.end(); ++l_it)
source_locationt source_location
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
ssize_t write(int fildes, const void *buf, size_t nbyte)