JBMC: run convert-nondet on a per-function basis

Author: smowton

src/goto-programs/convert_nondet.cpp

@@ -130,6 +130,20 @@ void convert_nondet(
   }
 }
 
+void convert_nondet(
+  goto_model_functiont &function,
+  message_handlert &message_handler,
+  const object_factory_parameterst &object_factory_parameters)
+{
+  convert_nondet(
+    function.get_goto_function().body,
+    function.get_symbol_table(),
+    message_handler,
+    object_factory_parameters);
+
+  function.compute_location_numbers();
+}
+
 void convert_nondet(
   goto_functionst &goto_functions,
   symbol_tablet &symbol_table,

src/goto-programs/convert_nondet.h

@@ -17,6 +17,7 @@ Author: Reuben Thomas, [email protected]
 class goto_functionst;
 class symbol_tablet;
 class goto_modelt;
+class goto_model_functiont;
 class message_handlert;
 struct object_factory_parameterst;
 
@@ -38,4 +39,15 @@ void convert_nondet(
   message_handlert &,
   const object_factory_parameterst &object_factory_parameters);
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation.
+/// \param function: goto program to modify
+/// \param message_handler: For error logging.
+/// \param object_factory_parameters: Parameters for the generation of nondet
+///   objects.
+void convert_nondet(
+  goto_model_functiont &function,
+  message_handlert &message_handler,
+  const object_factory_parameterst &object_factory_parameters);
+
 #endif

src/jbmc/jbmc_parse_options.cpp

@@ -666,6 +666,28 @@ void jbmc_parse_optionst::process_goto_function(
     remove_returns(function, function_is_stub);
 
     replace_java_nondet(function);
+
+    // Similar removal of java nondet statements:
+    // TODO Should really get this from java_bytecode_language somehow, but we
+    // don't have an instance of that here.
+    object_factory_parameterst factory_params;
+    factory_params.max_nondet_array_length=
+      cmdline.isset("java-max-input-array-length")
+        ? std::stoul(cmdline.get_value("java-max-input-array-length"))
+        : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
+    factory_params.max_nondet_string_length=
+      cmdline.isset("string-max-input-length")
+        ? std::stoul(cmdline.get_value("string-max-input-length"))
+        : MAX_NONDET_STRING_LENGTH;
+    factory_params.max_nondet_tree_depth=
+      cmdline.isset("java-max-input-tree-depth")
+        ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
+        : MAX_NONDET_TREE_DEPTH;
+
+    convert_nondet(
+      function,
+      get_message_handler(),
+      factory_params);
   }
 
   catch(const char *e)
@@ -703,28 +725,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // Similar removal of java nondet statements:
-    // TODO Should really get this from java_bytecode_language somehow, but we
-    // don't have an instance of that here.
-    object_factory_parameterst factory_params;
-    factory_params.max_nondet_array_length=
-      cmdline.isset("java-max-input-array-length")
-        ? std::stoul(cmdline.get_value("java-max-input-array-length"))
-        : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-    factory_params.max_nondet_string_length=
-      cmdline.isset("string-max-input-length")
-        ? std::stoul(cmdline.get_value("string-max-input-length"))
-        : MAX_NONDET_STRING_LENGTH;
-    factory_params.max_nondet_tree_depth=
-      cmdline.isset("java-max-input-tree-depth")
-        ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
-        : MAX_NONDET_TREE_DEPTH;
-
-    convert_nondet(
-      goto_model,
-      get_message_handler(),
-      factory_params);
-
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
     goto_check(options, goto_model);