Skip to content

Commit 9683cb5

Browse files
thk123thk123
authored
Merge pull request diffblue#919 from reuk/no-std-inheritance
Stop inheriting from std containers
2 parents df16159 + b00c377 commit 9683cb5

19 files changed

+433
-196
lines changed

‎src/analyses/goto_rw.h

Lines changed: 50 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,14 @@ void goto_rw(const goto_functionst &goto_functions,
4545
class range_domain_baset
4646
{
4747
public:
48+
range_domain_baset()=default;
49+
50+
range_domain_baset(const range_domain_baset &rhs)=delete;
51+
range_domain_baset &operator=(const range_domain_baset &rhs)=delete;
52+
53+
range_domain_baset(range_domain_baset &&rhs)=delete;
54+
range_domain_baset &operator=(range_domain_baset &&rhs)=delete;
55+
4856
virtual ~range_domain_baset();
4957

5058
virtual void output(const namespacet &ns, std::ostream &out) const=0;
@@ -62,12 +70,29 @@ inline range_spect to_range_spect(const mp_integer &size)
6270
}
6371

6472
// each element x represents a range of bits [x.first, x.second.first)
65-
class range_domaint:
66-
public range_domain_baset,
67-
public std::list<std::pair<range_spect, range_spect> >
73+
class range_domaint:public range_domain_baset
6874
{
75+
typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
76+
sub_typet data;
77+
6978
public:
70-
virtual void output(const namespacet &ns, std::ostream &out) const;
79+
void output(const namespacet &ns, std::ostream &out) const override;
80+
81+
// NOLINTNEXTLINE(readability/identifiers)
82+
typedef sub_typet::iterator iterator;
83+
// NOLINTNEXTLINE(readability/identifiers)
84+
typedef sub_typet::const_iterator const_iterator;
85+
86+
iterator begin() { return data.begin(); }
87+
const_iterator begin() const { return data.begin(); }
88+
const_iterator cbegin() const { return data.begin(); }
89+
90+
iterator end() { return data.end(); }
91+
const_iterator end() const { return data.end(); }
92+
const_iterator cend() const { return data.end(); }
93+
94+
template <typename T>
95+
void push_back(T &&v) { data.push_back(std::forward<T>(v)); }
7196
};
7297

7398
class array_exprt;
@@ -258,12 +283,29 @@ class rw_range_set_value_sett:public rw_range_sett
258283
const range_spect &size);
259284
};
260285

261-
class guarded_range_domaint:
262-
public range_domain_baset,
263-
public std::multimap<range_spect, std::pair<range_spect, exprt> >
286+
class guarded_range_domaint:public range_domain_baset
264287
{
288+
typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
289+
sub_typet data;
290+
265291
public:
266-
virtual void output(const namespacet &ns, std::ostream &out) const;
292+
virtual void output(const namespacet &ns, std::ostream &out) const override;
293+
294+
// NOLINTNEXTLINE(readability/identifiers)
295+
typedef sub_typet::iterator iterator;
296+
// NOLINTNEXTLINE(readability/identifiers)
297+
typedef sub_typet::const_iterator const_iterator;
298+
299+
iterator begin() { return data.begin(); }
300+
const_iterator begin() const { return data.begin(); }
301+
const_iterator cbegin() const { return data.begin(); }
302+
303+
iterator end() { return data.end(); }
304+
const_iterator end() const { return data.end(); }
305+
const_iterator cend() const { return data.end(); }
306+
307+
template<typename T>
308+
iterator insert(T &&v) { return data.insert(std::forward<T>(v)); }
267309
};
268310

269311
class rw_guarded_range_set_value_sett:public rw_range_set_value_sett

‎src/analyses/local_bitvector_analysis.cpp

Lines changed: 17 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,16 @@ void local_bitvector_analysist::flagst::print(std::ostream &out) const
4141
out << "+integer_address";
4242
}
4343

44-
bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
44+
bool local_bitvector_analysist::merge(points_tot &a, points_tot &b)
4545
{
4646
bool result=false;
4747

4848
std::size_t max_index=
49-
std::max(src.points_to.size(), points_to.size());
49+
std::max(a.size(), b.size());
5050

5151
for(std::size_t i=0; i<max_index; i++)
5252
{
53-
if(points_to[i].merge(src.points_to[i]))
53+
if(a[i].merge(b[i]))
5454
result=true;
5555
}
5656

@@ -72,8 +72,8 @@ bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
7272
void local_bitvector_analysist::assign_lhs(
7373
const exprt &lhs,
7474
const exprt &rhs,
75-
const loc_infot &loc_info_src,
76-
loc_infot &loc_info_dest)
75+
points_tot &loc_info_src,
76+
points_tot &loc_info_dest)
7777
{
7878
if(lhs.id()==ID_symbol)
7979
{
@@ -83,7 +83,7 @@ void local_bitvector_analysist::assign_lhs(
8383
{
8484
unsigned dest_pointer=pointers.number(identifier);
8585
flagst rhs_flags=get_rec(rhs, loc_info_src);
86-
loc_info_dest.points_to[dest_pointer]=rhs_flags;
86+
loc_info_dest[dest_pointer]=rhs_flags;
8787
}
8888
}
8989
else if(lhs.id()==ID_dereference)
@@ -117,14 +117,12 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get(
117117

118118
assert(loc_it!=cfg.loc_map.end());
119119

120-
const loc_infot &loc_info_src=loc_infos[loc_it->second];
121-
122-
return get_rec(rhs, loc_info_src);
120+
return get_rec(rhs, loc_infos[loc_it->second]);
123121
}
124122

125123
local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
126124
const exprt &rhs,
127-
const loc_infot &loc_info_src)
125+
points_tot &loc_info_src)
128126
{
129127
if(rhs.id()==ID_constant)
130128
{
@@ -139,7 +137,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
139137
if(is_tracked(identifier))
140138
{
141139
unsigned src_pointer=pointers.number(identifier);
142-
return loc_info_src.points_to[src_pointer];
140+
return loc_info_src[src_pointer];
143141
}
144142
else
145143
return flagst::mk_unknown();
@@ -258,7 +256,7 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
258256
// in the entry location.
259257
for(const auto &local : locals.locals_map)
260258
if(is_tracked(local.first))
261-
loc_infos[0].points_to[pointers.number(local.first)]=flagst::mk_unknown();
259+
loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown();
262260

263261
while(!work_queue.empty())
264262
{
@@ -267,8 +265,8 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
267265
const goto_programt::instructiont &instruction=*node.t;
268266
work_queue.pop();
269267

270-
const loc_infot &loc_info_src=loc_infos[loc_nr];
271-
loc_infot loc_info_dest=loc_infos[loc_nr];
268+
auto &loc_info_src=loc_infos[loc_nr];
269+
auto loc_info_dest=loc_infos[loc_nr];
272270

273271
switch(instruction.type)
274272
{
@@ -320,7 +318,7 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
320318
for(const auto &succ : node.successors)
321319
{
322320
assert(succ<loc_infos.size());
323-
if(loc_infos[succ].merge(loc_info_dest))
321+
if(merge(loc_infos[succ], (loc_info_dest)))
324322
work_queue.push(succ);
325323
}
326324
}
@@ -337,14 +335,14 @@ void local_bitvector_analysist::output(
337335
{
338336
out << "**** " << i_it->source_location << "\n";
339337

340-
const loc_infot &loc_info=loc_infos[l];
338+
const auto &loc_info=loc_infos[l];
341339

342340
for(points_tot::const_iterator
343-
p_it=loc_info.points_to.begin();
344-
p_it!=loc_info.points_to.end();
341+
p_it=loc_info.begin();
342+
p_it!=loc_info.end();
345343
p_it++)
346344
{
347-
out << " " << pointers[p_it-loc_info.points_to.begin()]
345+
out << " " << pointers[p_it-loc_info.begin()]
348346
<< ": "
349347
<< *p_it
350348
<< "\n";

‎src/analyses/local_bitvector_analysis.h

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -186,27 +186,20 @@ class local_bitvector_analysist
186186
// This is a vector, so it's fast.
187187
typedef expanding_vectort<flagst> points_tot;
188188

189-
// the information tracked per program location
190-
class loc_infot
191-
{
192-
public:
193-
points_tot points_to;
194-
195-
bool merge(const loc_infot &src);
196-
};
189+
static bool merge(points_tot &a, points_tot &b);
197190

198-
typedef std::vector<loc_infot> loc_infost;
191+
typedef std::vector<points_tot> loc_infost;
199192
loc_infost loc_infos;
200193

201194
void assign_lhs(
202195
const exprt &lhs,
203196
const exprt &rhs,
204-
const loc_infot &loc_info_src,
205-
loc_infot &loc_info_dest);
197+
points_tot &loc_info_src,
198+
points_tot &loc_info_dest);
206199

207200
flagst get_rec(
208201
const exprt &rhs,
209-
const loc_infot &loc_info_src);
202+
points_tot &loc_info_src);
210203

211204
bool is_tracked(const irep_idt &identifier);
212205
};

‎src/goto-instrument/wmm/cycle_collection.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ void event_grapht::graph_explorert::filter_thin_air(
2525
{
2626
std::set<critical_cyclet>::const_iterator next=it;
2727
++next;
28-
critical_cyclet::const_iterator e_it=it->begin();
28+
auto e_it=it->begin();
2929
/* is there an event in the cycle not in thin-air events? */
3030
for(; e_it!=it->end(); ++e_it)
3131
if(thin_air_events.find(*e_it)==thin_air_events.end())

‎src/goto-instrument/wmm/data_dp.cpp

Lines changed: 23 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Date: 2012
1313

1414
#include "data_dp.h"
1515

16+
#include <util/invariant.h>
1617
#include <util/message.h>
1718

1819
#include "abstract_event.h"
@@ -24,13 +25,13 @@ void data_dpt::dp_analysis(
2425
const datat &write,
2526
bool local_write)
2627
{
27-
const_iterator it;
28+
data_typet::const_iterator it;
2829

29-
for(it=begin(); it!=end(); ++it)
30+
for(it=data.cbegin(); it!=data.cend(); ++it)
3031
{
3132
if(local_read && it->id==read.id)
3233
{
33-
insert(
34+
data.insert(
3435
datat(
3536
write.id,
3637
(local_write?source_locationt():write.loc),
@@ -40,7 +41,7 @@ void data_dpt::dp_analysis(
4041

4142
if(local_write && it->id==write.id)
4243
{
43-
insert(
44+
data.insert(
4445
datat(
4546
read.id,
4647
(local_read?source_locationt():read.loc),
@@ -49,12 +50,12 @@ void data_dpt::dp_analysis(
4950
}
5051
}
5152

52-
if(it==end())
53+
if(it==data.cend())
5354
{
5455
++class_nb;
55-
insert(
56+
data.insert(
5657
datat(read.id, (local_read?source_locationt():read.loc), class_nb));
57-
insert(
58+
data.insert(
5859
datat(write.id, (local_write?source_locationt():write.loc), class_nb));
5960
}
6061
}
@@ -71,11 +72,11 @@ void data_dpt::dp_analysis(
7172
/// search in N^2
7273
bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
7374
{
74-
for(const_iterator it1=begin(); it1!=end(); ++it1)
75+
for(auto it1=data.cbegin(); it1!=data.cend(); ++it1)
7576
{
76-
const_iterator it2=it1;
77+
auto it2=it1;
7778
++it2;
78-
if(it2==end())
79+
if(it2==data.cend())
7980
break;
8081

8182
if(e1.local)
@@ -89,7 +90,7 @@ bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
8990
continue;
9091
}
9192

92-
for(; it2!=end(); ++it2)
93+
for(; it2!=data.cend(); ++it2)
9394
{
9495
if(e2.local)
9596
{
@@ -116,42 +117,42 @@ bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
116117
/// merge in N^3
117118
void data_dpt::dp_merge()
118119
{
119-
if(size()<2)
120+
if(data.size()<2)
120121
return;
121122

122-
unsigned initial_size=size();
123+
unsigned initial_size=data.size();
123124

124125
unsigned from=0;
125126
unsigned to=0;
126127

127128
/* look for similar elements */
128-
for(const_iterator it1=begin(); it1!=end(); ++it1)
129+
for(auto it1=data.cbegin(); it1!=data.cend(); ++it1)
129130
{
130-
const_iterator it2=it1;
131+
auto it2=it1;
131132
++it2;
132133
/* all ok -- ends */
133-
if(it2==end())
134+
if(it2==data.cend())
134135
return;
135136

136-
for(; it2!=end(); ++it2)
137+
for(; it2!=data.cend(); ++it2)
137138
{
138139
if(it1 == it2)
139140
{
140141
from=it2->eq_class;
141142
to=it1->eq_class;
142-
erase(it2);
143+
data.erase(it2);
143144
break;
144145
}
145146
}
146147
}
147148

148149
/* merge */
149-
for(iterator it3=begin(); it3!=end(); ++it3)
150+
for(auto it3=data.begin(); it3!=data.end(); ++it3)
150151
if(it3->eq_class==from)
151152
it3->eq_class=to;
152153

153154
/* strictly monotonous => converges */
154-
assert(initial_size>size());
155+
INVARIANT(initial_size>data.size(), "strictly monotonous => converges");
155156

156157
/* repeat until classes are disjunct */
157158
dp_merge();
@@ -160,10 +161,10 @@ void data_dpt::dp_merge()
160161
void data_dpt::print(messaget &message)
161162
{
162163
#ifdef DEBUG
163-
const_iterator it;
164+
data_typet::const_iterator it;
164165
std::map<unsigned, std::set<source_locationt> > classed;
165166

166-
for(it=begin(); it!=end(); ++it)
167+
for(it=data.cbegin(); it!=data.cend(); ++it)
167168
{
168169
if(classed.find(it->eq_class)==classed.end())
169170
{

‎src/goto-instrument/wmm/data_dp.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,11 +48,13 @@ struct datat
4848
}
4949
};
5050

51-
class data_dpt:public std::set<datat>
51+
class data_dpt final
5252
{
53-
public:
53+
typedef std::set<datat> data_typet;
54+
data_typet data;
5455
unsigned class_nb;
5556

57+
public:
5658
/* add this dependency in the structure */
5759
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write);
5860
void dp_analysis(

0 commit comments

Comments
 (0)