diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c
new file mode 100644
index 00000000000..9e557e515a7
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void func(int *p);
+
+void main()
+{
+  int *p;
+  p = NULL;
+
+  func(p);
+}
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc
new file mode 100644
index 00000000000..c81743d4d72
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --pointer-check
+^SIGNAL=0$
+^EXIT=0$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple/main.c b/regression/goto-instrument/generate-function-body-havoc-params-simple/main.c
new file mode 100644
index 00000000000..7a3cc50cbe1
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-simple/main.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void func(int *p);
+
+void main()
+{
+  int i;
+  i = 0;
+
+  func(&i);
+
+  assert(i == 0);
+}
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc
new file mode 100644
index 00000000000..e6f3f142cf5
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion i == 0: FAILURE
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c
new file mode 100644
index 00000000000..4c7270f7527
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c
@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st2 *to_st2;
+  int data;
+} st1_t;
+
+typedef struct st2
+{
+  struct st1 *to_st1;
+  int data;
+} st2_t;
+
+st1_t dummy1;
+st2_t dummy2;
+
+void func(st1_t *p);
+
+void main()
+{
+  st1_t st;
+
+  func(&st);
+
+  assert(st.to_st2 != NULL);
+  assert(st.to_st2->to_st1 != NULL);
+  assert(st.to_st2->to_st1->to_st2 == NULL);
+
+  assert(st.to_st2 != &dummy2);
+  assert(st.to_st2->to_st1 != &dummy1);
+}
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc
new file mode 100644
index 00000000000..d8dd403aba8
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options 'havoc,params:p' --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c
new file mode 100644
index 00000000000..44848513382
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  int data;
+} st_t;
+
+void func(st_t *p);
+
+void main()
+{
+  st_t st;
+  st.data = 0;
+
+  func(&st);
+
+  assert(st.data == 0);
+}
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc
new file mode 100644
index 00000000000..1f964d59ba4
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion st.data == 0: FAILURE
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c
new file mode 100644
index 00000000000..1a2dcac6a53
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c
@@ -0,0 +1,31 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  struct st *prev;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p);
+
+void main()
+{
+  st_t st;
+
+  func(&st);
+
+  assert(st.prev != NULL);
+  assert(st.prev != &dummy);
+
+  assert(st.next != NULL);
+  assert(st.next != &dummy);
+
+  assert(st.prev->prev == NULL);
+  assert(st.prev->next == NULL);
+  assert(st.next->prev == NULL);
+  assert(st.next->next == NULL);
+}
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc
new file mode 100644
index 00000000000..ed0a9f66c67
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c
new file mode 100644
index 00000000000..4d5f4c8d16b
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c
@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p);
+
+void main()
+{
+  st_t st;
+
+  func(&st);
+
+  assert(st.next != NULL);
+  assert(st.next->next != NULL);
+  assert(st.next->next->next == NULL);
+
+  assert(st.next != &dummy);
+  assert(st.next->next != &dummy);
+}
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc
new file mode 100644
index 00000000000..ac6ee2cc354
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index a6ce51d967a..ea08e404cb8 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -42,7 +42,8 @@ exprt::operandst build_function_environment(
       base_name,
       p.type(),
       p.source_location(),
-      object_factory_parameters);
+      object_factory_parameters,
+      lifetimet::AUTOMATIC_LOCAL);
   }
 
   return main_arguments;
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index ddb9162eb7c..f53b09b1d5a 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -25,79 +25,29 @@ Author: Diffblue Ltd.
 
 #include <goto-programs/goto_functions.h>
 
-class symbol_factoryt
-{
-  symbol_tablet &symbol_table;
-  const source_locationt &loc;
-  namespacet ns;
-  const c_object_factory_parameterst &object_factory_params;
-
-  allocate_objectst allocate_objects;
-
-  typedef std::set<irep_idt> recursion_sett;
-
-public:
-  symbol_factoryt(
-    symbol_tablet &_symbol_table,
-    const source_locationt &loc,
-    const c_object_factory_parameterst &object_factory_params)
-    : symbol_table(_symbol_table),
-      loc(loc),
-      ns(_symbol_table),
-      object_factory_params(object_factory_params),
-      allocate_objects(ID_C, loc, loc.get_function(), symbol_table)
-  {}
-
-  void gen_nondet_init(
-    code_blockt &assignments,
-    const exprt &expr,
-    const std::size_t depth = 0,
-    recursion_sett recursion_set = recursion_sett());
-
-  void add_created_symbol(const symbolt *symbol_ptr)
-  {
-    allocate_objects.add_created_symbol(symbol_ptr);
-  }
-
-  void declare_created_symbols(code_blockt &init_code)
-  {
-    allocate_objects.declare_created_symbols(init_code);
-  }
-
-  void mark_created_symbols_as_input(code_blockt &init_code)
-  {
-    allocate_objects.mark_created_symbols_as_input(init_code);
-  }
-
-private:
-  /// Generate initialisation code for each array element
-  /// \param assignments: The code block to add code to
-  /// \param expr: An expression of array type
-  /// \param depth: The struct recursion depth
-  /// \param recursion_set: The struct recursion set
-  /// \see gen_nondet_init For the meaning of the last 2 parameters
-  void gen_nondet_array_init(
-    code_blockt &assignments,
-    const exprt &expr,
-    std::size_t depth,
-    const recursion_sett &recursion_set);
-};
-
 /// Creates a nondet for expr, including calling itself recursively to make
 /// appropriate symbols to point to if expr is a pointer.
 /// \param assignments: The code block to add code to
 /// \param expr: The expression which we are generating a non-determinate value
 ///   for
-/// \param depth: number of pointers followed so far during initialisation
-/// \param recursion_set: names of structs seen so far on current pointer chain
+/// \param depth number of pointers followed so far during initialisation
+/// \param recursion_set names of structs seen so far on current pointer chain
+/// \param assign_const Indicates whether const objects should be nondet
+///   initialized
 void symbol_factoryt::gen_nondet_init(
   code_blockt &assignments,
   const exprt &expr,
   const std::size_t depth,
-  recursion_sett recursion_set)
+  recursion_sett recursion_set,
+  const bool assign_const)
 {
   const typet &type = expr.type();
 
+  if(!assign_const && expr.type().get_bool(ID_C_constant))
+  {
+    return;
+  }
+
   if(type.id()==ID_pointer)
   {
     // dereferenced type
@@ -120,10 +70,10 @@ void symbol_factoryt::gen_nondet_init(
 
     code_blockt non_null_inst;
 
-    exprt init_expr = allocate_objects.allocate_automatic_local_object(
-      non_null_inst, expr, subtype);
+    exprt init_expr =
+      allocate_objects.allocate_object(non_null_inst, expr, subtype, lifetime);
 
-    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set);
+    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
 
     if(depth < object_factory_params.min_null_tree_depth)
     {
@@ -165,12 +115,18 @@ void symbol_factoryt::gen_nondet_init(
     for(const auto &component : struct_type.components())
     {
       const typet &component_type = component.type();
+
+      if(!assign_const && component_type.get_bool(ID_C_constant))
+      {
+        continue;
+      }
+
       const irep_idt name = component.get_name();
 
       member_exprt me(expr, name, component_type);
       me.add_source_location() = loc;
 
-      gen_nondet_init(assignments, me, depth, recursion_set);
+      gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
     }
   }
   else if(type.id() == ID_array)
@@ -221,6 +177,8 @@ void symbol_factoryt::gen_nondet_array_init(
 /// \param loc: The location to assign to generated code
 /// \param object_factory_parameters: configuration parameters for the object
 ///   factory
+/// \param lifetime: Lifetime of the allocated object (AUTOMATIC_LOCAL,
+///   STATIC_GLOBAL, or DYNAMIC)
 /// \return Returns the symbol_exprt for the symbol created
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
@@ -228,7 +186,8 @@ symbol_exprt c_nondet_symbol_factory(
   const irep_idt base_name,
   const typet &type,
   const source_locationt &loc,
-  const c_object_factory_parameterst &object_factory_parameters)
+  const c_object_factory_parameterst &object_factory_parameters,
+  const lifetimet lifetime)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -247,7 +206,8 @@ symbol_exprt c_nondet_symbol_factory(
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
   CHECK_RETURN(!moving_symbol_failed);
 
-  symbol_factoryt state(symbol_table, loc, object_factory_parameters);
+  symbol_factoryt state(symbol_table, loc, object_factory_parameters, lifetime);
+
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 
diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
index c4d74f6021f..9ccda4d90f9 100644
--- a/src/ansi-c/c_nondet_symbol_factory.h
+++ b/src/ansi-c/c_nondet_symbol_factory.h
@@ -14,15 +14,84 @@ Author: Diffblue Ltd.
 
 #include "c_object_factory_parameters.h"
 
+#include <set>
+#include <vector>
+
+#include <util/allocate_objects.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+class symbol_factoryt
+{
+  symbol_tablet &symbol_table;
+  const source_locationt &loc;
+  namespacet ns;
+  const c_object_factory_parameterst &object_factory_params;
+
+  allocate_objectst allocate_objects;
+
+  const lifetimet lifetime;
+
+public:
+  typedef std::set<irep_idt> recursion_sett;
+
+  symbol_factoryt(
+    symbol_tablet &_symbol_table,
+    const source_locationt &loc,
+    const c_object_factory_parameterst &object_factory_params,
+    const lifetimet lifetime)
+    : symbol_table(_symbol_table),
+      loc(loc),
+      ns(_symbol_table),
+      object_factory_params(object_factory_params),
+      allocate_objects(ID_C, loc, loc.get_function(), symbol_table),
+      lifetime(lifetime)
+  {
+  }
+
+  void gen_nondet_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    const std::size_t depth = 0,
+    recursion_sett recursion_set = recursion_sett(),
+    const bool assign_const = true);
+
+  void add_created_symbol(const symbolt *symbol_ptr)
+  {
+    allocate_objects.add_created_symbol(symbol_ptr);
+  }
+
+  void declare_created_symbols(code_blockt &init_code)
+  {
+    allocate_objects.declare_created_symbols(init_code);
+  }
+
+  void mark_created_symbols_as_input(code_blockt &init_code)
+  {
+    allocate_objects.mark_created_symbols_as_input(init_code);
+  }
+
+private:
+  /// Generate initialisation code for each array element
+  /// \param assignments: The code block to add code to
+  /// \param expr: An expression of array type
+  /// \param depth: The struct recursion depth
+  /// \param recursion_set: The struct recursion set
+  /// \see gen_nondet_init For the meaning of the last 2 parameters
+  void gen_nondet_array_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    std::size_t depth,
+    const recursion_sett &recursion_set);
+};
+
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   const irep_idt base_name,
   const typet &type,
   const source_locationt &,
-  const c_object_factory_parameterst &object_factory_parameters);
+  const c_object_factory_parameterst &object_factory_parameters,
+  const lifetimet lifetime);
 
 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index c2bb06a36d0..6067aa4de8a 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -35,6 +35,7 @@ SRC = accelerate/accelerate.cpp \
       full_slicer.cpp \
       function.cpp \
       function_modifies.cpp \
+      generate_function_bodies.cpp \
       goto_instrument_languages.cpp \
       goto_instrument_main.cpp \
       goto_instrument_parse_options.cpp \
diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp
similarity index 75%
rename from src/goto-programs/generate_function_bodies.cpp
rename to src/goto-instrument/generate_function_bodies.cpp
index c7d45a3803f..b0dea5c7f88 100644
--- a/src/goto-programs/generate_function_bodies.cpp
+++ b/src/goto-instrument/generate_function_bodies.cpp
@@ -8,13 +8,17 @@ 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 <goto-programs/remove_skip.h>
+
 #include <util/arith_tools.h>
 #include <util/format_expr.h>
 #include <util/make_unique.h>
 #include <util/string_utils.h>
 
-#include "remove_skip.h"
-
 void generate_function_bodiest::generate_function_body(
   goto_functiont &function,
   symbol_tablet &symbol_table,
@@ -64,7 +68,7 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -87,7 +91,7 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -118,7 +122,7 @@ class assert_false_then_assume_false_generate_function_bodiest
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -146,115 +150,61 @@ class assert_false_then_assume_false_generate_function_bodiest
   }
 };
 
-class havoc_generate_function_bodiest : public generate_function_bodiest,
-                                        private messaget
+class havoc_generate_function_bodiest : public generate_function_bodiest
 {
 public:
   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),
+      message(message_handler)
   {
   }
 
 private:
   void havoc_expr_rec(
     const exprt &lhs,
-    const namespacet &ns,
-    const std::function<goto_programt::targett(void)> &add_instruction,
-    const irep_idt &function_name) const
+    const std::size_t initial_depth,
+    const source_locationt &source_location,
+    symbol_tablet &symbol_table,
+    goto_programt &dest) const
   {
-    // resolve type symbols
-    auto const lhs_type = ns.follow(lhs.type());
-    // skip constants
-    if(!lhs_type.get_bool(ID_C_constant))
-    {
-      // expand arrays, structs and union, everything else gets
-      // assigned nondet
-      if(lhs_type.id() == ID_struct || lhs_type.id() == ID_union)
-      {
-        // Note: In the case of unions it's often enough to assign
-        // just one member; However consider a case like
-        // union { struct { const int x; int y; } a;
-        //         struct {  int x; const int y; } b;};
-        // in this case both a.y and b.x must be assigned
-        // otherwise these parts stay constant even though
-        // they could've changed (note that type punning through
-        // unions is allowed in the C standard but forbidden in C++)
-        // so we're assigning all members even in the case of
-        // unions just to be safe
-        auto const lhs_struct_type = to_struct_union_type(lhs_type);
-        for(auto const &component : lhs_struct_type.components())
-        {
-          havoc_expr_rec(
-            member_exprt(lhs, component.get_name(), component.type()),
-            ns,
-            add_instruction,
-            function_name);
-        }
-      }
-      else if(lhs_type.id() == ID_array)
-      {
-        auto const lhs_array_type = to_array_type(lhs_type);
-        if(!lhs_array_type.subtype().get_bool(ID_C_constant))
-        {
-          bool constant_known_array_size = lhs_array_type.size().is_constant();
-          if(!constant_known_array_size)
-          {
-            warning() << "Cannot havoc non-const array " << format(lhs)
-                      << " in function " << function_name
-                      << ": Unknown array size" << eom;
-          }
-          else
-          {
-            auto const array_size =
-              numeric_cast<mp_integer>(lhs_array_type.size());
-            INVARIANT(
-              array_size.has_value(),
-              "Array size should be known constant integer");
-            if(array_size.value() == 0)
-            {
-              // Pretty much the same thing as a unknown size array
-              // Technically not allowed by the C standard, but we model
-              // unknown size arrays in structs this way
-              warning() << "Cannot havoc non-const array " << format(lhs)
-                        << " in function " << function_name << ": Array size 0"
-                        << eom;
-            }
-            else
-            {
-              for(mp_integer i = 0; i < array_size.value(); ++i)
-              {
-                auto const index =
-                  from_integer(i, lhs_array_type.size().type());
-                havoc_expr_rec(
-                  index_exprt(lhs, index, lhs_array_type.subtype()),
-                  ns,
-                  add_instruction,
-                  function_name);
-              }
-            }
-          }
-        }
-      }
-      else
-      {
-        auto assign_instruction = add_instruction();
-        assign_instruction->make_assignment(
-          code_assignt(
-            lhs, side_effect_expr_nondett(lhs_type, lhs.source_location())));
-      }
-    }
+    symbol_factoryt symbol_factory(
+      symbol_table,
+      source_location,
+      object_factory_parameters,
+      lifetimet::DYNAMIC);
+
+    code_blockt assignments;
+
+    symbol_factory.gen_nondet_init(
+      assignments,
+      lhs,
+      initial_depth,
+      symbol_factoryt::recursion_sett(),
+      false); // do not initialize const objects at the top level
+
+    code_blockt init_code;
+
+    symbol_factory.declare_created_symbols(init_code);
+    init_code.append(assignments);
+
+    goto_programt tmp_dest;
+    goto_convert(
+      init_code, symbol_table, tmp_dest, message.get_message_handler(), ID_C);
+
+    dest.destructive_append(tmp_dest);
   }
 
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -270,18 +220,29 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     {
       if(
         parameter.type().id() == ID_pointer &&
+        !parameter.type().subtype().get_bool(ID_C_constant) &&
         std::regex_match(
           id2string(parameter.get_base_name()), parameters_to_havoc))
       {
-        // if (param != nullptr) { *param = nondet(); }
         auto goto_instruction = add_instruction();
+
+        const irep_idt base_name = parameter.get_base_name();
+        CHECK_RETURN(!base_name.empty());
+
+        dereference_exprt dereference_expr(
+          symbol_exprt(parameter.get_identifier(), parameter.type()),
+          parameter.type().subtype());
+
+        goto_programt dest;
         havoc_expr_rec(
-          dereference_exprt(
-            symbol_exprt(parameter.get_identifier(), parameter.type()),
-            parameter.type().subtype()),
-          ns,
-          add_instruction,
-          function_name);
+          dereference_expr,
+          1, // depth 1 since we pass the dereferenced pointer
+          function_symbol.location,
+          symbol_table,
+          dest);
+
+        function.body.destructive_append(dest);
+
         auto label_instruction = add_instruction();
         goto_instruction->make_goto(
           label_instruction,
@@ -295,19 +256,25 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     for(auto const &global_id : globals_to_havoc)
     {
       auto const &global_sym = symbol_table.lookup_ref(global_id);
+
+      goto_programt dest;
+
       havoc_expr_rec(
         symbol_exprt(global_sym.name, global_sym.type),
-        ns,
-        add_instruction,
-        function_name);
+        0,
+        function_symbol.location,
+        symbol_table,
+        dest);
+
+      function.body.destructive_append(dest);
     }
+
     if(function.type.return_type() != void_typet())
     {
       auto return_instruction = add_instruction();
       return_instruction->make_return();
-      return_instruction->code = code_returnt(
-        side_effect_expr_nondett(
-          function.type.return_type(), function_symbol.location));
+      return_instruction->code = code_returnt(side_effect_expr_nondett(
+        function.type.return_type(), function_symbol.location));
     }
     auto end_function_instruction = add_instruction();
     end_function_instruction->make_end_function();
@@ -318,6 +285,8 @@ 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;
+  mutable messaget message;
 };
 
 class generate_function_bodies_errort : public std::runtime_error
@@ -333,13 +302,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")
@@ -408,7 +381,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 + "\"");
 }
diff --git a/src/goto-programs/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h
similarity index 95%
rename from src/goto-programs/generate_function_bodies.h
rename to src/goto-instrument/generate_function_bodies.h
index c909bb4bdd1..ebbb1dda05a 100644
--- a/src/goto-programs/generate_function_bodies.h
+++ b/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>
@@ -31,7 +32,7 @@ class generate_function_bodiest
   /// \param function_name: Identifier of function
   virtual void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const = 0;
 
 public:
@@ -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);
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index f4b29d43e02..7e191181b58 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/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>
 
@@ -1185,6 +1187,25 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     remove_skip(goto_model);
   }
 
+  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(
+      std::regex(cmdline.get_value("generate-function-body")),
+      *generate_implementation,
+      goto_model,
+      *message_handler);
+  }
+
   // add generic checks, if needed
   goto_check(options, goto_model);
 
@@ -1487,19 +1508,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       throw 0;
   }
 
-  if(cmdline.isset("generate-function-body"))
-  {
-    auto generate_implementation = generate_function_bodies_factory(
-      cmdline.get_value("generate-function-body-options"),
-      goto_model.symbol_table,
-      *message_handler);
-    generate_function_bodies(
-      std::regex(cmdline.get_value("generate-function-body")),
-      *generate_implementation,
-      goto_model,
-      *message_handler);
-  }
-
   // aggressive slicer
   if(cmdline.isset("aggressive-slice"))
   {
@@ -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"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index a5179302446..7e70a1ff1d7 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/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>
@@ -27,8 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
-#include <goto-programs/generate_function_bodies.h>
 #include "aggressive_slicer.h"
+#include "generate_function_bodies.h"
 
 #include "count_eloc.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
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index fdd55802453..da48da7c821 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -6,7 +6,6 @@ SRC = adjust_float_expressions.cpp \
       destructor.cpp \
       elf_reader.cpp \
       format_strings.cpp \
-      generate_function_bodies.cpp \
       goto_asm.cpp \
       goto_clean_expr.cpp \
       goto_convert.cpp \