Pass c object factory parameters to function body generation

Author: danpoe

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <memory>
 
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/json.h>
@@ -1187,8 +1189,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("generate-function-body"))
   {
+    optionst options;
+    parse_c_object_factory_options(cmdline, options);
+    c_object_factory_parameterst object_factory_parameters(options);
+
     auto generate_implementation = generate_function_bodies_factory(
       cmdline.get_value("generate-function-body-options"),
+      object_factory_parameters,
       goto_model.symbol_table,
       *message_handler);
     generate_function_bodies(

src/goto-instrument/goto_instrument_parse_options.h

@@ -104,6 +104,8 @@ Author: Daniel Kroening, [email protected]
   OPT_REPLACE_CALLS \
   "(validate-goto-binary)" \
   OPT_VALIDATE \
+  "(max-nondet-tree-depth):" \
+  "(min-null-tree-depth):" \
   // empty last line
 
 // clang-format on

src/goto-programs/generate_function_bodies.cpp

@@ -8,6 +8,11 @@ Author: Diffblue Ltd.
 
 #include "generate_function_bodies.h"
 
+#include <ansi-c/c_nondet_symbol_factory.h>
+#include <ansi-c/c_object_factory_parameters.h>
+
+#include <goto-programs/goto_convert.h>
+
 #include <util/arith_tools.h>
 #include <util/format_expr.h>
 #include <util/make_unique.h>
@@ -153,11 +158,13 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
   havoc_generate_function_bodiest(
     std::vector<irep_idt> globals_to_havoc,
     std::regex parameters_to_havoc,
+    const c_object_factory_parameterst &object_factory_parameters,
     message_handlert &message_handler)
     : generate_function_bodiest(),
       messaget(message_handler),
       globals_to_havoc(std::move(globals_to_havoc)),
-      parameters_to_havoc(std::move(parameters_to_havoc))
+      parameters_to_havoc(std::move(parameters_to_havoc)),
+      object_factory_parameters(object_factory_parameters)
   {
   }
 
@@ -318,6 +325,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
 private:
   const std::vector<irep_idt> globals_to_havoc;
   std::regex parameters_to_havoc;
+  const c_object_factory_parameterst &object_factory_parameters;
 };
 
 class generate_function_bodies_errort : public std::runtime_error
@@ -334,13 +342,17 @@ class generate_function_bodies_errort : public std::runtime_error
 ///                               parameter
 std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
   const std::string &options,
+  const c_object_factory_parameterst &object_factory_parameters,
   const symbol_tablet &symbol_table,
   message_handlert &message_handler)
 {
   if(options.empty() || options == "nondet-return")
   {
     return util_make_unique<havoc_generate_function_bodiest>(
-      std::vector<irep_idt>{}, std::regex{}, message_handler);
+      std::vector<irep_idt>{},
+      std::regex{},
+      object_factory_parameters,
+      message_handler);
   }
 
   if(options == "assume-false")
@@ -409,7 +421,10 @@ std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
       }
     }
     return util_make_unique<havoc_generate_function_bodiest>(
-      std::move(globals_to_havoc), std::move(params_regex), message_handler);
+      std::move(globals_to_havoc),
+      std::move(params_regex),
+      object_factory_parameters,
+      message_handler);
   }
   throw generate_function_bodies_errort("Can't parse \"" + options + "\"");
 }

src/goto-programs/generate_function_bodies.h

@@ -12,6 +12,7 @@ Author: Diffblue Ltd.
 #include <memory>
 #include <regex>
 
+#include <ansi-c/c_object_factory_parameters.h>
 #include <goto-programs/goto_function.h>
 #include <goto-programs/goto_model.h>
 #include <util/cmdline.h>
@@ -59,6 +60,7 @@ class generate_function_bodiest
 
 std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
   const std::string &options,
+  const c_object_factory_parameterst &object_factory_parameters,
   const symbol_tablet &symbol_table,
   message_handlert &message_handler);