Skip to content

Commit 5a41cb6

Browse files
tautschnigtautschnig
authored
Merge pull request #5615 from tautschnig/remove-forall-macros
Remove {f,F}orall_goto_functions
2 parents 261f598 + e8e0193 commit 5a41cb6

File tree

79 files changed

+516
-426
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

79 files changed

+516
-426
lines changed

‎.clang-format

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,6 @@ DerivePointerAlignment: 'false'
3030
DisableFormat: 'false'
3131
ExperimentalAutoDetectBinPacking: 'false'
3232
ForEachMacros: [
33-
'forall_goto_functions',
34-
'Forall_goto_functions',
3533
'forall_goto_program_instructions',
3634
'Forall_goto_program_instructions',
3735
'forall_operands',

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -558,13 +558,13 @@ int janalyzer_parse_optionst::perform_analysis(
558558
{
559559
namespacet ns(goto_model.symbol_table);
560560

561-
forall_goto_functions(it, goto_model.goto_functions)
561+
for(const auto &gf_entry : goto_model.goto_functions.function_map)
562562
{
563563
std::cout << ">>>>\n";
564-
std::cout << ">>>> " << it->first << '\n';
564+
std::cout << ">>>> " << gf_entry.first << '\n';
565565
std::cout << ">>>>\n";
566-
local_may_aliast local_may_alias(it->second);
567-
local_may_alias.output(std::cout, it->second, ns);
566+
local_may_aliast local_may_alias(gf_entry.second);
567+
local_may_alias.output(std::cout, gf_entry.second, ns);
568568
std::cout << '\n';
569569
}
570570

‎jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -619,8 +619,8 @@ void remove_exceptionst::instrument_exceptions(
619619

620620
void remove_exceptionst::operator()(goto_functionst &goto_functions)
621621
{
622-
Forall_goto_functions(it, goto_functions)
623-
instrument_exceptions(it->first, it->second.body);
622+
for(auto &gf_entry : goto_functions.function_map)
623+
instrument_exceptions(gf_entry.first, gf_entry.second.body);
624624
}
625625

626626
void remove_exceptionst::

‎jbmc/src/jdiff/java_syntactic_diff.cpp

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -16,25 +16,25 @@ Author: Peter Schrammel
1616

1717
bool java_syntactic_difft::operator()()
1818
{
19-
forall_goto_functions(it, goto_model1.goto_functions)
19+
for(const auto &gf_entry : goto_model1.goto_functions.function_map)
2020
{
21-
if(!it->second.body_available())
21+
if(!gf_entry.second.body_available())
2222
continue;
2323

2424
goto_functionst::function_mapt::const_iterator f_it =
25-
goto_model2.goto_functions.function_map.find(it->first);
25+
goto_model2.goto_functions.function_map.find(gf_entry.first);
2626
if(
2727
f_it == goto_model2.goto_functions.function_map.end() ||
2828
!f_it->second.body_available())
2929
{
30-
deleted_functions.insert(it->first);
30+
deleted_functions.insert(gf_entry.first);
3131
continue;
3232
}
3333

3434
// check access qualifiers
35-
const symbolt *fun1 = goto_model1.symbol_table.lookup(it->first);
35+
const symbolt *fun1 = goto_model1.symbol_table.lookup(gf_entry.first);
3636
CHECK_RETURN(fun1 != nullptr);
37-
const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first);
37+
const symbolt *fun2 = goto_model2.symbol_table.lookup(gf_entry.first);
3838
CHECK_RETURN(fun2 != nullptr);
3939
const optionalt<irep_idt> class_name = declaring_class(*fun1);
4040
bool function_access_changed =
@@ -67,29 +67,29 @@ bool java_syntactic_difft::operator()()
6767
}
6868
if(function_access_changed || class_access_changed || field_access_changed)
6969
{
70-
modified_functions.insert(it->first);
70+
modified_functions.insert(gf_entry.first);
7171
continue;
7272
}
7373

74-
if(!it->second.body.equals(f_it->second.body))
74+
if(!gf_entry.second.body.equals(f_it->second.body))
7575
{
76-
modified_functions.insert(it->first);
76+
modified_functions.insert(gf_entry.first);
7777
continue;
7878
}
7979
}
80-
forall_goto_functions(it, goto_model2.goto_functions)
80+
for(const auto &gf_entry : goto_model2.goto_functions.function_map)
8181
{
82-
if(!it->second.body_available())
82+
if(!gf_entry.second.body_available())
8383
continue;
8484

8585
total_functions_count++;
8686

8787
goto_functionst::function_mapt::const_iterator f_it =
88-
goto_model1.goto_functions.function_map.find(it->first);
88+
goto_model1.goto_functions.function_map.find(gf_entry.first);
8989
if(
9090
f_it == goto_model1.goto_functions.function_map.end() ||
9191
!f_it->second.body_available())
92-
new_functions.insert(it->first);
92+
new_functions.insert(gf_entry.first);
9393
}
9494

9595
return !(

‎src/analyses/ai.cpp

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -24,16 +24,16 @@ void ai_baset::output(
2424
const goto_functionst &goto_functions,
2525
std::ostream &out) const
2626
{
27-
forall_goto_functions(f_it, goto_functions)
27+
for(const auto &gf_entry : goto_functions.function_map)
2828
{
29-
if(f_it->second.body_available())
29+
if(gf_entry.second.body_available())
3030
{
3131
out << "////\n";
32-
out << "//// Function: " << f_it->first << "\n";
32+
out << "//// Function: " << gf_entry.first << "\n";
3333
out << "////\n";
3434
out << "\n";
3535

36-
output(ns, f_it->first, f_it->second.body, out);
36+
output(ns, gf_entry.first, gf_entry.second.body, out);
3737
}
3838
}
3939
}
@@ -64,16 +64,16 @@ jsont ai_baset::output_json(
6464
{
6565
json_objectt result;
6666

67-
forall_goto_functions(f_it, goto_functions)
67+
for(const auto &gf_entry : goto_functions.function_map)
6868
{
69-
if(f_it->second.body_available())
69+
if(gf_entry.second.body_available())
7070
{
71-
result[id2string(f_it->first)] =
72-
output_json(ns, f_it->first, f_it->second.body);
71+
result[id2string(gf_entry.first)] =
72+
output_json(ns, gf_entry.first, gf_entry.second.body);
7373
}
7474
else
7575
{
76-
result[id2string(f_it->first)]=json_arrayt();
76+
result[id2string(gf_entry.first)] = json_arrayt();
7777
}
7878
}
7979

@@ -111,17 +111,18 @@ xmlt ai_baset::output_xml(
111111
{
112112
xmlt program("program");
113113

114-
forall_goto_functions(f_it, goto_functions)
114+
for(const auto &gf_entry : goto_functions.function_map)
115115
{
116116
xmlt function(
117117
"function",
118-
{{"name", id2string(f_it->first)},
119-
{"body_available", f_it->second.body_available() ? "true" : "false"}},
118+
{{"name", id2string(gf_entry.first)},
119+
{"body_available", gf_entry.second.body_available() ? "true" : "false"}},
120120
{});
121121

122-
if(f_it->second.body_available())
122+
if(gf_entry.second.body_available())
123123
{
124-
function.new_element(output_xml(ns, f_it->first, f_it->second.body));
124+
function.new_element(
125+
output_xml(ns, gf_entry.first, gf_entry.second.body));
125126
}
126127

127128
program.new_element(function);
@@ -194,8 +195,8 @@ void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program)
194195

195196
void ai_baset::initialize(const goto_functionst &goto_functions)
196197
{
197-
forall_goto_functions(it, goto_functions)
198-
initialize(it->first, it->second);
198+
for(const auto &gf_entry : goto_functions.function_map)
199+
initialize(gf_entry.first, gf_entry.second);
199200
}
200201

201202
void ai_baset::finalize()

‎src/analyses/ai.h

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -706,20 +706,23 @@ class concurrency_aware_ait:public ait<domainT>
706706
typedef std::list<wl_entryt> thread_wlt;
707707
thread_wlt thread_wl;
708708

709-
forall_goto_functions(it, goto_functions)
710-
forall_goto_program_instructions(t_it, it->second.body)
709+
for(const auto &gf_entry : goto_functions.function_map)
710+
{
711+
forall_goto_program_instructions(t_it, gf_entry.second.body)
711712
{
712713
if(is_threaded(t_it))
713714
{
714-
thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
715+
thread_wl.push_back(
716+
wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
715717

716718
goto_programt::const_targett l_end =
717-
it->second.body.instructions.end();
719+
gf_entry.second.body.instructions.end();
718720
--l_end;
719721

720722
merge_shared(shared_state, l_end, sh_target, ns);
721723
}
722724
}
725+
}
723726

724727
// now feed in the shared state into all concurrently executing
725728
// functions, and iterate until the shared state stabilizes

‎src/analyses/call_graph.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -39,10 +39,10 @@ call_grapht::call_grapht(
3939
const goto_functionst &goto_functions, bool collect_callsites):
4040
collect_callsites(collect_callsites)
4141
{
42-
forall_goto_functions(f_it, goto_functions)
42+
for(const auto &gf_entry : goto_functions.function_map)
4343
{
44-
const irep_idt &function_name = f_it->first;
45-
const goto_programt &body = f_it->second.body;
44+
const irep_idt &function_name = gf_entry.first;
45+
const goto_programt &body = gf_entry.second.body;
4646
nodes.insert(function_name);
4747
add(function_name, body);
4848
}

‎src/analyses/constant_propagator.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -741,8 +741,8 @@ void constant_propagator_ait::replace(
741741
goto_functionst &goto_functions,
742742
const namespacet &ns)
743743
{
744-
Forall_goto_functions(f_it, goto_functions)
745-
replace(f_it->second, ns);
744+
for(auto &gf_entry : goto_functions.function_map)
745+
replace(gf_entry.second, ns);
746746
}
747747

748748

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -776,19 +776,19 @@ void custom_bitvector_analysist::check(
776776
{
777777
unsigned pass=0, fail=0, unknown=0;
778778

779-
forall_goto_functions(f_it, goto_model.goto_functions)
779+
for(const auto &gf_entry : goto_model.goto_functions.function_map)
780780
{
781-
if(!f_it->second.body.has_assertion())
782-
continue;
781+
if(!gf_entry.second.body.has_assertion())
782+
continue;
783783

784784
// TODO this is a hard-coded hack
785-
if(f_it->first=="__actual_thread_spawn")
785+
if(gf_entry.first == "__actual_thread_spawn")
786786
continue;
787787

788788
if(!use_xml)
789-
out << "******** Function " << f_it->first << '\n';
789+
out << "******** Function " << gf_entry.first << '\n';
790790

791-
forall_goto_program_instructions(i_it, f_it->second.body)
791+
forall_goto_program_instructions(i_it, gf_entry.second.body)
792792
{
793793
exprt result;
794794
irep_idt description;
@@ -836,7 +836,7 @@ void custom_bitvector_analysist::check(
836836
out << ", " << description;
837837
out << ": ";
838838
const namespacet ns(goto_model.symbol_table);
839-
out << from_expr(ns, f_it->first, result);
839+
out << from_expr(ns, gf_entry.first, result);
840840
out << '\n';
841841
}
842842

‎src/analyses/dirty.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,8 @@ class dirtyt
9090
{
9191
// dirtyts should not be initialized twice
9292
PRECONDITION(!initialized);
93-
forall_goto_functions(it, goto_functions)
94-
build(it->second);
93+
for(const auto &gf_entry : goto_functions.function_map)
94+
build(gf_entry.second);
9595
initialized = true;
9696
}
9797

‎src/analyses/escape_analysis.cpp

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -463,9 +463,9 @@ void escape_analysist::instrument(
463463
{
464464
const namespacet ns(goto_model.symbol_table);
465465

466-
Forall_goto_functions(f_it, goto_model.goto_functions)
466+
for(auto &gf_entry : goto_model.goto_functions.function_map)
467467
{
468-
Forall_goto_program_instructions(i_it, f_it->second.body)
468+
Forall_goto_program_instructions(i_it, gf_entry.second.body)
469469
{
470470
get_state(i_it);
471471

@@ -478,7 +478,12 @@ void escape_analysist::instrument(
478478
std::set<irep_idt> cleanup_functions;
479479
operator[](i_it).check_lhs(code_assign.lhs(), cleanup_functions);
480480
insert_cleanup(
481-
f_it->second, i_it, code_assign.lhs(), cleanup_functions, false, ns);
481+
gf_entry.second,
482+
i_it,
483+
code_assign.lhs(),
484+
cleanup_functions,
485+
false,
486+
ns);
482487
}
483488
else if(instruction.type == DEAD)
484489
{
@@ -504,9 +509,14 @@ void escape_analysist::instrument(
504509
d.check_lhs(code_dead.symbol(), cleanup_functions2);
505510

506511
insert_cleanup(
507-
f_it->second, i_it, code_dead.symbol(), cleanup_functions1, true, ns);
512+
gf_entry.second,
513+
i_it,
514+
code_dead.symbol(),
515+
cleanup_functions1,
516+
true,
517+
ns);
508518
insert_cleanup(
509-
f_it->second,
519+
gf_entry.second,
510520
i_it,
511521
code_dead.symbol(),
512522
cleanup_functions2,

‎src/analyses/flow_insensitive_analysis.cpp

Lines changed: 10 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -60,11 +60,12 @@ void flow_insensitive_analysis_baset::output(
6060
const goto_functionst &goto_functions,
6161
std::ostream &out)
6262
{
63-
forall_goto_functions(f_it, goto_functions)
63+
for(const auto &gf_entry : goto_functions.function_map)
6464
{
65-
out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
65+
out << "////\n"
66+
<< "//// Function: " << gf_entry.first << "\n////\n\n";
6667

67-
output(f_it->first, f_it->second.body, out);
68+
output(gf_entry.first, gf_entry.second.body, out);
6869
}
6970
}
7071

@@ -383,20 +384,14 @@ void flow_insensitive_analysis_baset::fixedpoint(
383384
{
384385
// do each function at least once
385386

386-
forall_goto_functions(it, goto_functions)
387-
if(functions_done.find(it->first)==
388-
functions_done.end())
387+
for(const auto &gf_entry : goto_functions.function_map)
388+
{
389+
if(functions_done.find(gf_entry.first) == functions_done.end())
389390
{
390-
fixedpoint(it, goto_functions);
391+
functions_done.insert(gf_entry.first);
392+
fixedpoint(gf_entry.first, gf_entry.second.body, goto_functions);
391393
}
392-
}
393-
394-
bool flow_insensitive_analysis_baset::fixedpoint(
395-
const goto_functionst::function_mapt::const_iterator it,
396-
const goto_functionst &goto_functions)
397-
{
398-
functions_done.insert(it->first);
399-
return fixedpoint(it->first, it->second.body, goto_functions);
394+
}
400395
}
401396

402397
void flow_insensitive_analysis_baset::update(const goto_functionst &)

‎src/analyses/flow_insensitive_analysis.h

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -172,10 +172,6 @@ class flow_insensitive_analysis_baset
172172
const goto_programt &goto_program,
173173
const goto_functionst &goto_functions);
174174

175-
bool fixedpoint(
176-
goto_functionst::function_mapt::const_iterator it,
177-
const goto_functionst &goto_functions);
178-
179175
void fixedpoint(
180176
const goto_functionst &goto_functions);
181177

0 commit comments

Comments
 (0)