JBMC: run replace-Java-nondet on function-by-function basis

Author: smowton

src/goto-programs/replace_java_nondet.cpp

@@ -235,6 +235,16 @@ static void replace_java_nondet(goto_programt &goto_program)
   }
 }
 
+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);
+}
+
 void replace_java_nondet(goto_functionst &goto_functions)
 {
   for(auto &goto_program : goto_functions.function_map)

src/goto-programs/replace_java_nondet.h

@@ -14,6 +14,7 @@ Author: Reuben Thomas, [email protected]
 
 class goto_modelt;
 class goto_functionst;
+class goto_model_functiont;
 
 /// Replace calls to nondet library functions with an internal nondet
 /// representation.
@@ -22,4 +23,9 @@ void replace_java_nondet(goto_modelt &);
 
 void replace_java_nondet(goto_functionst &);
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation in a single function.
+/// \param function: The goto program to modify.
+void replace_java_nondet(goto_model_functiont &function);
+
 #endif

src/jbmc/jbmc_parse_options.cpp

@@ -651,6 +651,8 @@ void jbmc_parse_optionst::process_goto_function(
     remove_virtual_functions(function);
     // remove returns
     remove_returns(function);
+
+    replace_java_nondet(function);
   }
 
   catch(const char *e)
@@ -705,8 +707,6 @@ bool jbmc_parse_optionst::process_goto_functions(
         ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
         : MAX_NONDET_TREE_DEPTH;
 
-    replace_java_nondet(goto_model);
-
     convert_nondet(
       goto_model,
       get_message_handler(),