Skip to content

Commit 04b4f63

Browse files
Merge pull request #186 from diffblue/cleanup/misc
Cleanup
2 parents 498718f + 577fa6c commit 04b4f63

File tree

7 files changed

+33
-57
lines changed

7 files changed

+33
-57
lines changed

src/goto-analyzer/taint_analysis.cpp

+3-6
Original file line numberDiff line numberDiff line change
@@ -272,8 +272,7 @@ bool taint_analysist::operator()(
272272
end.add_instruction(END_FUNCTION);
273273

274274
forall_goto_functions(f_it, goto_functions)
275-
if(f_it->second.body_available() &&
276-
f_it->first!=goto_functionst::entry_point())
275+
if(f_it->second.body_available())
277276
{
278277
goto_programt::targett t=calls.add_instruction();
279278
code_function_callt call;
@@ -284,14 +283,12 @@ bool taint_analysist::operator()(
284283
g->make_goto(t, side_effect_expr_nondett(bool_typet()));
285284
}
286285

287-
goto_functionst::goto_functiont &entry=
288-
goto_functions.function_map[goto_functionst::entry_point()];
289-
286+
goto_functionst::goto_functiont entry;
290287
goto_programt &body=entry.body;
291-
292288
body.destructive_append(gotos);
293289
body.destructive_append(calls);
294290
body.destructive_append(end);
291+
goto_functions.function_map.emplace(goto_functionst::entry_point(), std::move(entry));
295292

296293
goto_functions.update();
297294
}

src/goto-instrument/thread_instrumentation.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ void thread_exit_instrumentation(goto_functionst &goto_functions)
7878
// now instrument
7979
for(const auto &fkt : thread_fkts)
8080
{
81-
thread_exit_instrumentation(goto_functions.function_map[fkt].body);
81+
thread_exit_instrumentation(goto_functions.function_map.at(fkt).body);
8282
}
8383
}
8484

src/goto-instrument/wmm/goto2graph.cpp

+8-11
Original file line numberDiff line numberDiff line change
@@ -175,12 +175,12 @@ void instrumentert::cfg_visitort::visit_cfg_function(
175175

176176
#ifdef LOCAL_MAY
177177
local_may_aliast local_may(
178-
instrumenter.goto_functions.function_map[function]);
178+
instrumenter.goto_functions.function_map.at(function));
179179
#endif
180180

181181
/* goes through the function */
182182
Forall_goto_program_instructions(i_it,
183-
instrumenter.goto_functions.function_map[function].body)
183+
instrumenter.goto_functions.function_map.at(function).body)
184184
{
185185
goto_programt::instructiont &instruction=*i_it;
186186

@@ -274,15 +274,15 @@ void instrumentert::cfg_visitort::visit_cfg_function(
274274
egraph.map_data_dp.insert(new_dp);
275275
data_dp.print(instrumenter.message);
276276

277-
if(instrumenter.goto_functions.function_map[function]
277+
if(instrumenter.goto_functions.function_map.at(function)
278278
.body.instructions.empty())
279279
{
280280
/* empty set of ending edges */
281281
}
282282
else
283283
{
284284
goto_programt::instructionst::iterator it=instrumenter
285-
.goto_functions.function_map[function].body.instructions.end();
285+
.goto_functions.function_map.at(function).body.instructions.end();
286286
--it;
287287
ending_vertex=in_pos[it];
288288
}
@@ -319,7 +319,7 @@ void inline instrumentert::cfg_visitort::visit_cfg_reference_function(
319319

320320
/* gets the body of the function */
321321
goto_programt::instructionst &body=instrumenter.goto_functions
322-
.function_map[id_function].body.instructions;
322+
.function_map.at(id_function).body.instructions;
323323

324324
if(body.empty())
325325
return;
@@ -502,7 +502,7 @@ void inline instrumentert::cfg_visitort::visit_cfg_duplicate(
502502
{
503503
instrumenter.message.status() << "Duplication..." << messaget::eom;
504504
const goto_functionst::goto_functiont &fun=
505-
instrumenter.goto_functions.function_map[i_it->function];
505+
instrumenter.goto_functions.function_map.at(i_it->function);
506506

507507
bool found_pos=false;
508508
goto_programt::const_targett new_targ=targ;
@@ -1300,15 +1300,12 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
13001300
}
13011301

13021302
/* now test whether this part of the code can exist */
1303-
goto_functionst::function_mapt map;
1303+
goto_functionst this_interleaving;
13041304
goto_function_templatet<goto_programt> one_interleaving;
13051305
one_interleaving.body.copy_from(interleaving);
1306-
map.insert(std::make_pair(
1306+
this_interleaving.function_map.insert(std::make_pair(
13071307
goto_functionst::entry_point(),
13081308
std::move(one_interleaving)));
1309-
1310-
goto_functionst this_interleaving;
1311-
this_interleaving.function_map=std::move(map);
13121309
optionst no_option;
13131310
null_message_handlert no_message;
13141311

src/goto-instrument/wmm/shared_buffers.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1058,7 +1058,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
10581058
return;
10591059

10601060
namespacet ns(symbol_table);
1061-
goto_programt &goto_program=goto_functions.function_map[function].body;
1061+
goto_programt &goto_program=goto_functions.function_map.at(function).body;
10621062

10631063
#ifdef LOCAL_MAY
10641064
local_may_aliast local_may(goto_functions.function_map[function]);

src/goto-programs/goto_functions_template.h

+8-21
Original file line numberDiff line numberDiff line change
@@ -185,42 +185,29 @@ template <class bodyT>
185185
void goto_functions_templatet<bodyT>::compute_location_numbers()
186186
{
187187
unsigned nr=0;
188-
189-
for(typename function_mapt::iterator
190-
it=function_map.begin();
191-
it!=function_map.end();
192-
it++)
193-
it->second.body.compute_location_numbers(nr);
188+
for(auto &named_function : function_map)
189+
named_function.second.body.compute_location_numbers(nr);
194190
}
195191

196192
template <class bodyT>
197193
void goto_functions_templatet<bodyT>::compute_incoming_edges()
198194
{
199-
for(typename function_mapt::iterator
200-
it=function_map.begin();
201-
it!=function_map.end();
202-
it++)
203-
it->second.body.compute_incoming_edges();
195+
for(auto &named_function : function_map)
196+
named_function.second.body.compute_incoming_edges();
204197
}
205198

206199
template <class bodyT>
207200
void goto_functions_templatet<bodyT>::compute_target_numbers()
208201
{
209-
for(typename function_mapt::iterator
210-
it=function_map.begin();
211-
it!=function_map.end();
212-
it++)
213-
it->second.body.compute_target_numbers();
202+
for(auto &named_function : function_map)
203+
named_function.second.body.compute_target_numbers();
214204
}
215205

216206
template <class bodyT>
217207
void goto_functions_templatet<bodyT>::compute_loop_numbers()
218208
{
219-
for(typename function_mapt::iterator
220-
it=function_map.begin();
221-
it!=function_map.end();
222-
it++)
223-
it->second.body.compute_loop_numbers();
209+
for(auto &named_function : function_map)
210+
named_function.second.body.compute_loop_numbers();
224211
}
225212

226213
#endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H

src/goto-programs/read_goto_binary.cpp

+5-10
Original file line numberDiff line numberDiff line change
@@ -255,22 +255,17 @@ static bool link_functions(
255255
goto_functionst::function_mapt::iterator dest_f_it=
256256
dest_functions.function_map.find(final_id);
257257

258+
goto_functionst::goto_functiont &src_func=src_it->second;
258259
if(dest_f_it==dest_functions.function_map.end()) // not there yet
259260
{
260-
rename_symbols_in_function(src_it->second, rename_symbol);
261-
262-
goto_functionst::goto_functiont &in_dest_symbol_table=
263-
dest_functions.function_map[final_id];
264-
265-
in_dest_symbol_table.body.swap(src_it->second.body);
266-
in_dest_symbol_table.type=src_it->second.type;
261+
rename_symbols_in_function(src_func, rename_symbol);
262+
dest_functions.function_map.insert(
263+
std::make_pair(final_id, std::move(src_func)));
267264
}
268265
else // collision!
269266
{
270267
goto_functionst::goto_functiont &in_dest_symbol_table=
271-
dest_functions.function_map[final_id];
272-
273-
goto_functionst::goto_functiont &src_func=src_it->second;
268+
dest_f_it->second;
274269

275270
if(in_dest_symbol_table.body.instructions.empty() ||
276271
weak_symbols.find(final_id)!=weak_symbols.end())

src/util/symbol_table.cpp

+7-7
Original file line numberDiff line numberDiff line change
@@ -45,23 +45,23 @@ bool symbol_tablet::add(const symbolt &symbol)
4545
/// location in the symbol table
4646
bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
4747
{
48-
symbolt tmp;
49-
48+
// Add an empty symbol to the table or retrieve existing symbol with same name
5049
std::pair<symbolst::iterator, bool> result=
51-
symbols.insert(std::pair<irep_idt, symbolt>(symbol.name, tmp));
50+
symbols.emplace(symbol.name, symbolt());
5251

5352
if(!result.second)
5453
{
54+
// Return the address of the symbol that already existed in the table
5555
new_symbol=&result.first->second;
5656
return true;
5757
}
5858

59-
symbol_base_map.insert(
60-
std::pair<irep_idt, irep_idt>(symbol.base_name, symbol.name));
61-
symbol_module_map.insert(
62-
std::pair<irep_idt, irep_idt>(symbol.module, symbol.name));
59+
symbol_base_map.emplace(symbol.base_name, symbol.name);
60+
symbol_module_map.emplace(symbol.module, symbol.name);
6361

62+
// Move the provided symbol into the symbol table
6463
result.first->second.swap(symbol);
64+
// Return the address of the new symbol in the table
6565
new_symbol=&result.first->second;
6666

6767
return false;

0 commit comments

Comments
 (0)