Skip to content

Commit 9e68466

Browse files
committed
Replace loop_id parameter with const instructiont&
1 parent dbff05b commit 9e68466

File tree

5 files changed

+22
-27
lines changed

5 files changed

+22
-27
lines changed

src/cbmc/symex_bmc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ bool symex_bmct::get_unwind(
108108
const symex_targett::sourcet &source,
109109
unsigned unwind)
110110
{
111-
const irep_idt id=goto_programt::loop_id(source.pc);
111+
const irep_idt id=goto_programt::loop_id(*source.pc);
112112

113113
// We use the most specific limit we have,
114114
// and 'infinity' when we have none.

src/goto-programs/goto_functions_template.h

Lines changed: 16 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -185,42 +185,37 @@ 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 &func : function_map)
189+
{
190+
func.second.body.compute_location_numbers(nr);
191+
}
194192
}
195193

196194
template <class bodyT>
197195
void goto_functions_templatet<bodyT>::compute_incoming_edges()
198196
{
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();
197+
for(auto &func : function_map)
198+
{
199+
func.second.body.compute_incoming_edges();
200+
}
204201
}
205202

206203
template <class bodyT>
207204
void goto_functions_templatet<bodyT>::compute_target_numbers()
208205
{
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();
206+
for(auto &func : function_map)
207+
{
208+
func.second.body.compute_target_numbers();
209+
}
214210
}
215211

216212
template <class bodyT>
217213
void goto_functions_templatet<bodyT>::compute_loop_numbers()
218214
{
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();
215+
for(auto &func : function_map)
216+
{
217+
func.second.body.compute_loop_numbers();
218+
}
224219
}
225220

226221
#endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H

src/goto-programs/goto_program_template.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -529,10 +529,10 @@ class goto_program_templatet
529529
void update();
530530

531531
/// Human-readable loop name
532-
static irep_idt loop_id(const_targett target)
532+
static irep_idt loop_id(const instructiont &instruction)
533533
{
534-
return id2string(target->function)+"."+
535-
std::to_string(target->loop_number);
534+
return id2string(instruction.function)+"."+
535+
std::to_string(instruction.loop_number);
536536
}
537537

538538
/// Is the program empty?

src/goto-symex/symex_goto.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ void goto_symext::symex_goto(statet &state)
7878
}
7979

8080
unsigned &unwind=
81-
frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count;
81+
frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
8282
unwind++;
8383

8484
// continue unwinding?

src/goto-symex/symex_main.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ void goto_symext::symex_transition(
4040
if(i_e->is_goto() && i_e->is_backwards_goto() &&
4141
(!is_backwards_goto ||
4242
state.source.pc->location_number>i_e->location_number))
43-
frame.loop_iterations[goto_programt::loop_id(i_e)].count=0;
43+
frame.loop_iterations[goto_programt::loop_id(*i_e)].count=0;
4444
}
4545

4646
state.source.pc=to;

0 commit comments

Comments
 (0)