Pass c object factory parameters to function body generation

Parse the c object factory command line parameters when the function body
generation is enabled, and pass the resulting c_object_factory_parameterst
object along to an appropriate subclass of generate_function_bodiest.

Author: danpoe

src/goto-instrument/generate_function_bodies.cpp

@@ -157,11 +157,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)
   {
   }
 
@@ -322,6 +324,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
@@ -337,13 +340,17 @@ class generate_function_bodies_errort : public std::runtime_error
 /// \see generate_function_bodies for the syntax of the options 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")
@@ -412,7 +419,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-instrument/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);
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -64,6 +64,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/is_threaded.h>
 #include <analyses/local_safe_pointers.h>
 
+#include <ansi-c/ansi_c_language.h>
+#include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
 #include <cpp/cprover_library.h>
 
@@ -1187,8 +1189,14 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("generate-function-body"))
   {
+    optionst c_object_factory_options;
+    parse_c_object_factory_options(cmdline, c_object_factory_options);
+    c_object_factory_parameterst object_factory_parameters(
+      c_object_factory_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(
@@ -1622,6 +1630,7 @@ void goto_instrument_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     "                              convert each call to an undefined function to assume(false)\n"
     HELP_REPLACE_FUNCTION_BODY
+    HELP_ANSI_C_LANGUAGE
     "\n"
     "Loop transformations:\n"
     " --k-induction <k>            check loops with k-induction\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
 
+#include <ansi-c/ansi_c_language.h>
+
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -104,6 +106,7 @@ Author: Daniel Kroening, kroening@kroening.com
   OPT_REPLACE_CALLS \
   "(validate-goto-binary)" \
   OPT_VALIDATE \
+  OPT_ANSI_C_LANGUAGE \
   // empty last line
 
 // clang-format on