File tree 2 files changed +1
-9
lines changed
2 files changed +1
-9
lines changed Original file line number Diff line number Diff line change @@ -288,8 +288,6 @@ void replace_java_nondet(goto_model_functiont &function)
288
288
goto_programt &program = function.get_goto_function ().body ;
289
289
replace_java_nondet (program);
290
290
291
- function.compute_location_numbers ();
292
-
293
291
remove_skip (program);
294
292
}
295
293
@@ -300,8 +298,6 @@ void replace_java_nondet(goto_functionst &goto_functions)
300
298
replace_java_nondet (goto_program.second .body );
301
299
}
302
300
303
- goto_functions.compute_location_numbers ();
304
-
305
301
remove_skip (goto_functions);
306
302
}
307
303
Original file line number Diff line number Diff line change @@ -536,11 +536,7 @@ void remove_virtual_functions(goto_model_functiont &function)
536
536
class_hierarchyt class_hierarchy;
537
537
class_hierarchy (function.get_symbol_table ());
538
538
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 );
544
540
}
545
541
546
542
void remove_virtual_function (
You can’t perform that action at this time.
0 commit comments