Remove redundant calls to compute_{location,loop}_numbers

NathanJPhillips · Jun 4, 2018 · 533775c · 533775c
1 parent e9cdffd
commit 533775c
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 9 deletions.
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -288,8 +288,6 @@ void replace_java_nondet(goto_model_functiont &function)
   goto_programt &program = function.get_goto_function().body;
   replace_java_nondet(program);
 
-  function.compute_location_numbers();
-
   remove_skip(program);
 }
 
@@ -300,8 +298,6 @@ void replace_java_nondet(goto_functionst &goto_functions)
     replace_java_nondet(goto_program.second.body);
   }
 
-  goto_functions.compute_location_numbers();
-
   remove_skip(goto_functions);
 }
 

diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
@@ -536,11 +536,7 @@ void remove_virtual_functions(goto_model_functiont &function)
   class_hierarchyt class_hierarchy;
   class_hierarchy(function.get_symbol_table());
   remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
-  bool changed = rvf.remove_virtual_functions(
-    function.get_goto_function().body);
-  // Give fresh location numbers to `function`, in case it has grown:
-  if(changed)
-    function.compute_location_numbers();
+  rvf.remove_virtual_functions(function.get_goto_function().body);
 }
 
 void remove_virtual_function(