Skip to content

Commit f4bb8d4

Browse files
committed
Remove redundant calls to compute_{location,loop}_numbers
1 parent c49e6d7 commit f4bb8d4

File tree

3 files changed

+1
-10
lines changed

3 files changed

+1
-10
lines changed

src/goto-instrument/model_argc_argv.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -182,7 +182,6 @@ bool model_argc_argv(
182182

183183
// update counters etc.
184184
remove_skip(start);
185-
start.compute_loop_numbers();
186185
goto_model.goto_functions.update();
187186

188187
return false;

src/goto-programs/remove_virtual_functions.cpp

+1-5
Original file line numberDiff line numberDiff line change
@@ -536,11 +536,7 @@ void remove_virtual_functions(goto_model_functiont &function)
536536
class_hierarchyt class_hierarchy;
537537
class_hierarchy(function.get_symbol_table());
538538
remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
539-
bool changed = rvf.remove_virtual_functions(
540-
function.get_goto_function().body);
541-
// Give fresh location numbers to `function`, in case it has grown:
542-
if(changed)
543-
function.compute_location_numbers();
539+
rvf.remove_virtual_functions(function.get_goto_function().body);
544540
}
545541

546542
void remove_virtual_function(

src/java_bytecode/replace_java_nondet.cpp

-4
Original file line numberDiff line numberDiff line change
@@ -288,8 +288,6 @@ void replace_java_nondet(goto_model_functiont &function)
288288
goto_programt &program = function.get_goto_function().body;
289289
replace_java_nondet(program);
290290

291-
function.compute_location_numbers();
292-
293291
remove_skip(program);
294292
}
295293

@@ -300,8 +298,6 @@ void replace_java_nondet(goto_functionst &goto_functions)
300298
replace_java_nondet(goto_program.second.body);
301299
}
302300

303-
goto_functions.compute_location_numbers();
304-
305301
remove_skip(goto_functions);
306302
}
307303

0 commit comments

Comments
 (0)