diff --git a/regression/cbmc/pointer-to-array-function-parameters-max-size/test.c b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.c
new file mode 100644
index 00000000000..ae83a9f6c48
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+void test(int *arr, int sz)
+{
+  assert(sz <= 10);
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}
diff --git a/regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc
new file mode 100644
index 00000000000..eaddb5de044
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --max-dynamic-array-size 20 --pointer-check --unwind 20 --associated-array-sizes arr:sz
+\[test.assertion.1\] line \d+ assertion sz <= 10: FAILURE
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+EXIT=10
+SIGNAL=0
diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c
new file mode 100644
index 00000000000..3afac1ef068
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int is_prefix_of(
+  const char *string,
+  int string_size,
+  const char *prefix,
+  int prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+
+  for(int ix = 0; ix < prefix_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}
diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc
new file mode 100644
index 00000000000..29a23f608ca
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc
@@ -0,0 +1,6 @@
+CORE
+test.c
+--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 20
+SIGNAL=0
+EXIT=0
+VERIFICATION SUCCESSFUL
diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c
new file mode 100644
index 00000000000..6500af4f123
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stddef.h>
+
+int is_prefix_of(
+  const char *string,
+  size_t string_size,
+  const char *prefix,
+  size_t prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+  assert(prefix_size <= string_size);
+  // oh no! we should have used prefix_size here
+  for(int ix = 0; ix < string_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}
diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc
new file mode 100644
index 00000000000..280b5c4c832
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 10
+EXIT=10
+SIGNAL=0
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+VERIFICATION FAILED
diff --git a/regression/cbmc/pointer-to-array-function-parameters-with-size/test.c b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.c
new file mode 100644
index 00000000000..436baadd23d
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.c
@@ -0,0 +1,7 @@
+void test(int *arr, int sz)
+{
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}
diff --git a/regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc
new file mode 100644
index 00000000000..18faa5c7c81
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 10 --associated-array-sizes arr:sz
+EXIT=0
+SIGNAL=0
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
diff --git a/regression/cbmc/pointer-to-array-function-parameters/test.c b/regression/cbmc/pointer-to-array-function-parameters/test.c
new file mode 100644
index 00000000000..f70cbfbae28
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters/test.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void test(int *arr)
+{
+  // works because the arrays we generate have at least one element
+  arr[0] = 5;
+
+  // doesn't work because our arrays have at most ten elements
+  arr[10] = 10;
+}
diff --git a/regression/cbmc/pointer-to-array-function-parameters/test.desc b/regression/cbmc/pointer-to-array-function-parameters/test.desc
new file mode 100644
index 00000000000..079e897d7b4
--- /dev/null
+++ b/regression/cbmc/pointer-to-array-function-parameters/test.desc
@@ -0,0 +1,6 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 20
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.12\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+--
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index 9453c077af4..eec59ce3ef5 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@@ -49,6 +49,8 @@ rm Quantifiers-invalid-var-range/test.desc
 rm Quantifiers-type/test.desc
 rm Union_Initialization1/test.desc
 rm address_space_size_limit1/test.desc
+rm address_space_size_limit3/test.desc
+rm argv1/test.desc
 rm array-function-parameters/test.desc
 rm array-tests/test.desc
 rm bounds_check1/test.desc
@@ -68,6 +70,15 @@ rm memory_allocation1/test.desc
 rm pointer-function-parameters-struct-mutual-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion-2/test.desc
+rm pointer-function-parameters-struct-simple-recursion-3/test.desc
+rm pointer-to-array-function-parameters-max-size/test.desc
+rm pointer-to-array-function-parameters-multi-arg-right/test.desc
+rm pointer-to-array-function-parameters-multi-arg-wrong/test.desc
+rm pointer-to-array-function-parameters-with-size/test.desc
+rm pointer-to-array-function-parameters/test.desc
+rm read1/test.desc
+rm realloc1/test.desc
+rm realloc2/test.desc
 rm scanf1/test.desc
 rm stack-trace/test.desc
 rm struct6/test.desc
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index a6ce51d967a..03df46ccf11 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -27,7 +27,7 @@ exprt::operandst build_function_environment(
 {
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
-
+  std::map<irep_idt, irep_idt> deferred_array_sizes;
   for(std::size_t param_number=0;
       param_number<parameters.size();
       param_number++)
@@ -42,7 +42,8 @@ exprt::operandst build_function_environment(
       base_name,
       p.type(),
       p.source_location(),
-      object_factory_parameters);
+      object_factory_parameters,
+      deferred_array_sizes);
   }
 
   return main_arguments;
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index d554dbb9d0c..724aa76071b 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -22,13 +22,26 @@ Author: Daniel Kroening, kroening@kroening.com
 // clang-format off
 #define OPT_ANSI_C_LANGUAGE \
   "(max-nondet-tree-depth):" \
-  "(min-null-tree-depth):"
+  "(min-null-tree-depth):" \
+  "(pointers-to-treat-as-arrays):" \
+  "(associated-array-sizes):" \
+  "(max-dynamic-array-size):" \
 
 #define HELP_ANSI_C_LANGUAGE \
   " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\
   "                              at level N pointers are set to null\n" \
   " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */\
-  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */
+  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */\
+  " --pointers-to-treat-as-arrays <identifier,...>  comma separated list of\n" \
+  "                               identifiers that should be initialized as arrays\n" /* NOLINT(*) */ \
+  " --associated-array-sizes <identifier:identifier...>\n" \
+  "                               comma separated list of colon separated pairs\n" /* NOLINT(*) */ \
+  "                               of identifiers; The first element of the pair \n" /* NOLINT(*) */ \
+  "                               should be the name of an array pointer \n" \
+  "                               (see --pointers-to-treat-as-arrays),\n" \
+  "                               the second an integer parameter that\n" \
+  "                               should hold its size\n" \
+  " --max-dynamic-array-size <size>  max size for dynamically allocated arrays\n" /* NOLINT(*) */
 // clang-format on
 
 class ansi_c_languaget:public languaget
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index ddb9162eb7c..b833b84729a 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -15,24 +15,30 @@ Author: Diffblue Ltd.
 
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
+#include <util/array_name.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
 #include <util/nondet_bool.h>
+#include <util/optional_utils.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 
 #include <goto-programs/goto_functions.h>
 
+#include <functional>
+
 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;
+  std::map<irep_idt, irep_idt> &deferred_array_sizes;
 
   typedef std::set<irep_idt> recursion_sett;
 
@@ -40,14 +46,26 @@ class symbol_factoryt
   symbol_factoryt(
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
-    const c_object_factory_parameterst &object_factory_params)
+    const c_object_factory_parameterst &object_factory_params,
+    std::map<irep_idt, irep_idt> &deferred_array_sizes)
     : 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)
+      allocate_objects(ID_C, loc, loc.get_function(), symbol_table),
+      deferred_array_sizes(deferred_array_sizes)
   {}
 
+  /// Generate a function that behaves like malloc from our stdlib
+  /// implementation
+  /// \param malloc_symbol_name The name of the malloc function
+  const symbolt &gen_malloc_function(const irep_idt &malloc_symbol_name);
+
+  void gen_array_allocation(
+    code_blockt &assignments,
+    const exprt &array_expr,
+    const exprt &size);
+
   void gen_nondet_init(
     code_blockt &assignments,
     const exprt &expr,
@@ -81,6 +99,62 @@ class symbol_factoryt
     const exprt &expr,
     std::size_t depth,
     const recursion_sett &recursion_set);
+
+  /// Type for functions that initialise array elements
+  /// \see gen_nondet_size_array_init
+  using gen_array_initialization_t = std::function<void(
+    code_blockt &assignments,
+    const exprt &array,
+    const exprt &array_size,
+    std::size_t depth,
+    const recursion_sett &recursion_set)>;
+
+  /// Generate code to nondet-initialize each element of an array
+  /// \param assignments: The code block the initialization statements
+  ///                     are written to
+  /// \param array: The expression representing the array type
+  /// \param depth: Struct initialisation recursion depth, \see gen_nondet_init
+  /// \param recursion_set: Struct initialisation recursion set
+  /// \param gen_array_initialization: A function that generates
+  ///          initialisation code for array members
+  void gen_nondet_size_array_init(
+    code_blockt &assignments,
+    const symbol_exprt &array,
+    const size_t depth,
+    const symbol_factoryt::recursion_sett &recursion_set,
+    const gen_array_initialization_t &gen_array_initialization);
+
+  /// Initialize each element of an array to nondet
+  /// \see gen_array_initialization_t
+  void gen_nondet_array_member_initialization(
+    code_blockt &assignments,
+    const exprt &array,
+    const exprt &array_size,
+    std::size_t depth,
+    const recursion_sett &recursion_set);
+
+  /// Remember to initialise a variable representing array size to the given
+  /// concrete size.
+  /// When generating array initialisation code we often have the case where we
+  /// have a pointer that should be initialised to be pointing to some array,
+  /// and some integer type variable that should hold its size. Sometimes when
+  /// generating the array initialisation code we haven't "seen" the size
+  /// variable yet (i.e. it is not yet in the symbol table and doesn't have
+  /// initialisation code generated for it yet). If that's the case we remember
+  /// that we have to set it to the right size later with this method.
+  /// \param associated_size_name: The name of variable that should be set to
+  ///         the right size
+  /// \param array_size_name: The name of the variable that holds the size
+  void defer_size_initialization(
+    irep_idt associated_size_name,
+    irep_idt array_size_name);
+
+  /// Return the name of a variable holding an array size if one is associated
+  /// with the given symbol name
+  optionalt<irep_idt> get_deferred_size(irep_idt symbol_name) const;
+
+  /// Lookup symbol expression in symbol table and get its base name
+  const irep_idt &get_symbol_base_name(const symbol_exprt &symbol_expr) const;
 };
 
 /// Creates a nondet for expr, including calling itself recursively to make
@@ -100,6 +174,34 @@ void symbol_factoryt::gen_nondet_init(
 
   if(type.id()==ID_pointer)
   {
+    if(expr.id() == ID_symbol)
+    {
+      auto const &symbol_expr = to_symbol_expr(expr);
+      const auto &symbol_name = get_symbol_base_name(symbol_expr);
+      using std::placeholders::_1;
+      using std::placeholders::_2;
+      using std::placeholders::_3;
+      using std::placeholders::_4;
+      using std::placeholders::_5;
+      if(object_factory_params.should_be_treated_as_array(symbol_name))
+      {
+        gen_array_initialization_t gen_array_initialization = std::bind(
+          &symbol_factoryt::gen_nondet_array_member_initialization,
+          this,
+          _1,
+          _2,
+          _3,
+          _4,
+          _5);
+        gen_nondet_size_array_init(
+          assignments,
+          symbol_expr,
+          depth,
+          recursion_set,
+          gen_array_initialization);
+        return;
+      }
+    }
     // dereferenced type
     const pointer_typet &pointer_type=to_pointer_type(type);
     const typet &subtype = pointer_type.subtype();
@@ -187,11 +289,93 @@ void symbol_factoryt::gen_nondet_init(
                                        : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
-
+    if(expr.id() == ID_symbol)
+    {
+      // check if this variable is meant to hold the size of a
+      // dynamically allocated array; If it is, set the value to the length
+      // of that array instead of leaving it nondet
+      auto const &symbol_expr = to_symbol_expr(expr);
+      auto const deferred_array_size =
+        get_deferred_size(get_symbol_base_name(symbol_expr));
+      if(deferred_array_size.has_value())
+      {
+        assign.rhs() = typecast_exprt{
+          symbol_table.lookup_ref(deferred_array_size.value()).symbol_expr(),
+          symbol_expr.type()};
+      }
+    }
     assignments.add(std::move(assign));
   }
 }
 
+const irep_idt &
+symbol_factoryt::get_symbol_base_name(const symbol_exprt &symbol_expr) const
+{
+  return symbol_table.lookup_ref(symbol_expr.get_identifier()).base_name;
+}
+
+void symbol_factoryt::gen_nondet_size_array_init(
+  code_blockt &assignments,
+  const symbol_exprt &array,
+  const size_t depth,
+  const symbol_factoryt::recursion_sett &recursion_set,
+  const gen_array_initialization_t &gen_array_initialization)
+{
+  // This works on dynamic arrays, so the thing we assign to is a pointer
+  // rather than an array with a fixed size
+  PRECONDITION(array.type().id() == ID_pointer);
+
+  // Overall, create code that roughly does this:
+  // size_t size;
+  // T *array;
+  // size = choose_in_range(1, max_array_size);
+  // array = malloc(sizeof(T) * size);
+  // nondet_fill_T(array, size);
+  // where nondet_fill_T is responsible for setting up the values of the array,
+  // for example nondet-initialiasing them
+  auto const max_array_size = object_factory_params.max_dynamic_array_size;
+  auto const &array_name = get_symbol_base_name(array);
+  auto const &size_symbol = allocate_objects.allocate_automatic_local_object(
+    size_type(), CPROVER_PREFIX "nondet_array_size");
+
+  // assume (1 <= size && size <= max_array_size)
+  auto size_initialization = code_assumet{
+    and_exprt{binary_exprt{
+                from_integer(1, size_type()), ID_le, size_symbol, bool_typet{}},
+              binary_exprt{size_symbol,
+                           ID_le,
+                           from_integer(max_array_size, size_type()),
+                           bool_typet{}}}};
+
+  assignments.add(size_initialization);
+  gen_array_allocation(assignments, array, size_symbol);
+  gen_array_initialization(
+    assignments, array, size_symbol, depth, recursion_set);
+  // if we've already initialised the associated array size,
+  // then set the associated array size to the size of the generated array
+  // otherwise, defer the initialisation of the associated array size
+  auto const associated_size =
+    object_factory_params.get_associated_size_variable(array_name);
+  if(associated_size.has_value())
+  {
+    auto const associated_size_symbol =
+      symbol_table.lookup(associated_size.value());
+    if(associated_size_symbol != nullptr)
+    {
+      assignments.add(code_assignt{
+        associated_size_symbol->symbol_expr(),
+        typecast_exprt{size_symbol, associated_size_symbol->type}});
+    }
+    else
+    {
+      // we've not seen the associated size symbol yet, so we have
+      // to defer setting it to when we do get there...
+      defer_size_initialization(
+        associated_size.value(), size_symbol.get_identifier());
+    }
+  }
+}
+
 void symbol_factoryt::gen_nondet_array_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -211,6 +395,224 @@ void symbol_factoryt::gen_nondet_array_init(
   }
 }
 
+const symbolt &
+symbol_factoryt::gen_malloc_function(const irep_idt &malloc_symbol_name)
+{
+  // the name passed in as parameter should not exist in the symbol
+  // table already
+  PRECONDITION(symbol_table.lookup(malloc_symbol_name) == nullptr);
+
+  auto source_location = source_locationt{};
+  source_location.set_file(
+    "<builtin-library-" + id2string(malloc_symbol_name) + ">");
+  symbolt malloc_sym;
+  malloc_sym.base_name = malloc_sym.name = malloc_sym.pretty_name =
+    malloc_symbol_name;
+  malloc_sym.mode = "C";
+
+  auto malloc_body = code_blockt{};
+  malloc_body.add_source_location() = source_location;
+
+  // create a new local variable with this name and type, and return
+  // a symbol_expr that represents this variable
+  auto declare_local_variable = [&](
+                                  const std::string &name, const typet &type) {
+    auto const local_id = irep_idt{id2string(malloc_symbol_name) + "::" + name};
+    auto local_sym = symbolt{};
+    local_sym.type = type;
+    local_sym.pretty_name = name;
+    local_sym.name = id2string(local_id);
+    local_sym.base_name = name;
+    local_sym.is_lvalue = false;
+    local_sym.is_static_lifetime = false;
+    local_sym.is_type = false;
+    local_sym.mode = "C";
+    symbol_table.insert(local_sym);
+    malloc_body.add(code_declt{local_sym.symbol_expr()});
+    return local_sym.symbol_expr();
+  };
+
+  // declare the parameter `size_t malloc_size` for malloc
+  auto malloc_size_param_symbol = symbolt{};
+  malloc_size_param_symbol.type = size_type();
+  malloc_size_param_symbol.name =
+    id2string(malloc_symbol_name) + "::malloc_size";
+  malloc_size_param_symbol.pretty_name = "malloc_size";
+  malloc_size_param_symbol.base_name = "malloc_size";
+  malloc_size_param_symbol.is_static_lifetime = false;
+  malloc_size_param_symbol.is_parameter = true;
+  symbol_table.insert(malloc_size_param_symbol);
+  auto malloc_size_param = code_typet::parametert{size_type()};
+  malloc_size_param.set_base_name("malloc_size");
+  malloc_size_param.set_identifier(malloc_size_param_symbol.name);
+
+  // the signature for our malloc is
+  // void *__CPROVER_malloc(size_t malloc_size);
+  malloc_sym.type = code_typet{code_typet::parameterst{malloc_size_param},
+                               pointer_type(void_type())};
+
+  auto const &local_size_variable = malloc_size_param_symbol.symbol_expr();
+
+  // the variable that holds the allocation result, i.e. a valid void*
+  // that points to a memory region of malloc_size bytes
+  // void *malloc_res = __CPROVER_allocate(malloc_size, 0);
+  auto const malloc_res =
+    declare_local_variable("malloc_res", pointer_type(void_type()));
+
+  // the actual allocation
+  auto malloc_allocate = side_effect_exprt{ID_allocate};
+  malloc_allocate.copy_to_operands(local_size_variable);
+  malloc_allocate.copy_to_operands(false_exprt{});
+  malloc_body.add(code_assignt{malloc_res, malloc_allocate});
+
+  // the following are all setting various CBMC book-keeping variables
+
+  // __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
+  auto const &cprover_deallocated =
+    symbol_table.lookup_ref(CPROVER_PREFIX "deallocated");
+  malloc_body.add(code_assignt{
+    cprover_deallocated.symbol_expr(),
+    if_exprt{equal_exprt{malloc_res, cprover_deallocated.symbol_expr()},
+             from_integer(0, cprover_deallocated.type),
+             cprover_deallocated.symbol_expr()}});
+
+  // __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
+  auto const record_malloc =
+    declare_local_variable("record_malloc", bool_typet{});
+  malloc_body.add(
+    code_assignt{record_malloc, get_nondet_bool(bool_typet{}, loc)});
+
+  // __CPROVER_malloc_object=record_malloc?malloc_res:__CPROVER_malloc_object;
+  auto const &malloc_object =
+    symbol_table.lookup_ref(CPROVER_PREFIX "malloc_object");
+  malloc_body.add(code_assignt{malloc_object.symbol_expr(),
+                               if_exprt{record_malloc,
+                                        malloc_res,
+                                        malloc_object.symbol_expr(),
+                                        malloc_object.type}});
+
+  // __CPROVER_malloc_size=record_malloc?malloc_size:__CPROVER_malloc_size;
+  auto const &malloc_size =
+    symbol_table.lookup_ref(CPROVER_PREFIX "malloc_size");
+  malloc_body.add(code_assignt{malloc_size.symbol_expr(),
+                               if_exprt{record_malloc,
+                                        local_size_variable,
+                                        malloc_size.symbol_expr(),
+                                        malloc_size.type}});
+
+  // __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
+  auto const &malloc_is_new_array =
+    symbol_table.lookup_ref(CPROVER_PREFIX "malloc_is_new_array");
+  malloc_body.add(code_assignt{
+    malloc_is_new_array.symbol_expr(),
+    if_exprt{record_malloc, false_exprt{}, malloc_is_new_array.symbol_expr()}});
+
+  // __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
+  auto const record_may_leak =
+    declare_local_variable("record_may_leak", bool_typet{});
+  malloc_body.add(code_declt{record_may_leak});
+  malloc_body.add(
+    code_assignt{record_may_leak, get_nondet_bool(bool_typet{}, loc)});
+
+  // __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak;
+  auto const &memory_leak =
+    symbol_table.lookup_ref(CPROVER_PREFIX "memory_leak");
+  malloc_body.add(code_assignt{
+    memory_leak.symbol_expr(),
+    if_exprt{record_may_leak, malloc_res, memory_leak.symbol_expr()}});
+
+  // return malloc_res;
+  malloc_body.add(code_returnt{malloc_res});
+
+  malloc_sym.value = malloc_body;
+  auto inserted_sym = symbol_table.insert(malloc_sym);
+
+  // since the function is only called when there's no symbol with
+  // malloc_sym.name already in the symbol table, inserting it does succeed
+  CHECK_RETURN(inserted_sym.second);
+  return inserted_sym.first;
+}
+
+void symbol_factoryt::defer_size_initialization(
+  irep_idt associated_size_name,
+  irep_idt array_size_name)
+{
+  auto succeeded =
+    deferred_array_sizes.insert({associated_size_name, array_size_name});
+  INVARIANT(
+    succeeded.second,
+    "each size parameter should have a unique associated array");
+}
+
+optionalt<irep_idt>
+symbol_factoryt::get_deferred_size(irep_idt symbol_name) const
+{
+  return optional_lookup(deferred_array_sizes, symbol_name);
+}
+
+/// Generates a statement that allocates an array with a certain number of
+/// elements
+/// \param assignments: Where the statement is being written to
+/// \param array_expr: An expression representing a pointer to an array
+/// \param size: The number of elements to allocate for the array
+void symbol_factoryt::gen_array_allocation(
+  code_blockt &assignments,
+  const exprt &array_expr,
+  const exprt &size)
+{
+  PRECONDITION(array_expr.type().id() == ID_pointer);
+  irep_idt malloc_symbol_name = CPROVER_PREFIX "malloc";
+  auto const *malloc_symbol = symbol_table.lookup(malloc_symbol_name);
+  if(!malloc_symbol)
+  {
+    malloc_symbol = &gen_malloc_function(malloc_symbol_name);
+  }
+  auto const &element_type = array_expr.type().subtype();
+  const exprt &array_size = size_of_expr(array_typet{element_type, size}, ns);
+
+  // array = malloc(sizeof(array[size]))
+  auto allocate_array =
+    side_effect_expr_function_callt{malloc_symbol->symbol_expr(),
+                                    exprt::operandst{array_size},
+                                    array_expr.type(),
+                                    loc};
+  assignments.add(code_assignt{array_expr, allocate_array});
+}
+
+void symbol_factoryt::gen_nondet_array_member_initialization(
+  code_blockt &assignments,
+  const exprt &array,
+  const exprt &array_size,
+  std::size_t depth,
+  const symbol_factoryt::recursion_sett &recursion_set)
+{
+  // for(size_t ix = 0; ix < size; ++ix) {
+  //   arr[ix] = nondet_init_T();
+  // }
+
+  auto const &array_index_symbol =
+    allocate_objects.allocate_automatic_local_object(size_type(), "index");
+  auto array_member_init = code_fort{};
+
+  array_member_init.init() =
+    code_assignt{array_index_symbol, from_integer(0, size_type())};
+
+  array_member_init.cond() =
+    binary_exprt{array_index_symbol, ID_lt, array_size, bool_typet{}};
+
+  auto array_member_init_body = code_blockt{};
+  gen_nondet_init(
+    array_member_init_body,
+    dereference_exprt{plus_exprt{array, array_index_symbol, array.type()}},
+    depth + 1,
+    recursion_set);
+  array_member_init_body.add(code_assignt{
+    array_index_symbol,
+    plus_exprt{array_index_symbol, from_integer(1, size_type()), size_type()}});
+  array_member_init.body() = std::move(array_member_init_body);
+  assignments.add(std::move(array_member_init));
+}
+
 /// Creates a symbol and generates code so that it can vary over all possible
 /// values for its type. For pointers this involves allocating symbols which it
 /// can point to.
@@ -221,6 +623,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 deferred_array_sizes: A map of size parameter name -> symbol
+///        that holds the value the parameter should be assigned to
 /// \return Returns the symbol_exprt for the symbol created
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
@@ -228,7 +632,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,
+  std::map<irep_idt, irep_idt> &deferred_array_sizes)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -247,7 +652,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, deferred_array_sizes);
   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..2dd2b75dd39 100644
--- a/src/ansi-c/c_nondet_symbol_factory.h
+++ b/src/ansi-c/c_nondet_symbol_factory.h
@@ -22,7 +22,8 @@ symbol_exprt c_nondet_symbol_factory(
   symbol_tablet &symbol_table,
   const irep_idt base_name,
   const typet &type,
-  const source_locationt &,
-  const c_object_factory_parameterst &object_factory_parameters);
+  const source_locationt &loc,
+  const c_object_factory_parameterst &object_factory_parameters,
+  std::map<irep_idt, irep_idt> &deferred_array_sizes);
 
 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
diff --git a/src/ansi-c/c_object_factory_parameters.cpp b/src/ansi-c/c_object_factory_parameters.cpp
index 4634dc5aeee..0f06d70aa4a 100644
--- a/src/ansi-c/c_object_factory_parameters.cpp
+++ b/src/ansi-c/c_object_factory_parameters.cpp
@@ -8,7 +8,118 @@ Author: Daniel Poetzl
 
 #include "c_object_factory_parameters.h"
 
+#include <util/cmdline.h>
+#include <util/exception_utils.h>
+#include <util/optional_utils.h>
+#include <util/string_utils.h>
+
+#include <algorithm>
+#include <iterator>
+#include <string>
+
 void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
 {
   parse_object_factory_options(cmdline, options);
+  if(cmdline.isset("pointers-to-treat-as-arrays"))
+  {
+    options.set_option(
+      "pointers-to-treat-as-arrays",
+      cmdline.get_comma_separated_values("pointers-to-treat-as-arrays"));
+  }
+  if(cmdline.isset("associated-array-sizes"))
+  {
+    options.set_option(
+      "associated-array-sizes",
+      cmdline.get_comma_separated_values("associated-array-sizes"));
+  }
+  if(cmdline.isset("max-dynamic-array-size"))
+  {
+    options.set_option(
+      "max-dynamic-array-size", cmdline.get_value("max-dynamic-array-size"));
+  }
+}
+
+void c_object_factory_parameterst::set(const optionst &options)
+{
+  object_factory_parameterst::set(options);
+  auto const &pointers_to_treat_as_array =
+    options.get_list_option("pointers-to-treat-as-arrays");
+  std::transform(
+    std::begin(pointers_to_treat_as_array),
+    std::end(pointers_to_treat_as_array),
+    std::inserter(
+      this->pointers_to_treat_as_array, this->pointers_to_treat_as_array.end()),
+    id2string);
+
+  if(options.is_set("max-dynamic-array-size"))
+  {
+    max_dynamic_array_size =
+      options.get_unsigned_int_option("max-dynamic-array-size");
+    if(max_dynamic_array_size == 0)
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "Max dynamic array size must be >= 1", "--max-dynamic-array-size");
+    }
+  }
+  if(options.is_set("associated-array-sizes"))
+  {
+    array_name_to_associated_array_size_variable.clear();
+    variables_that_hold_array_sizes.clear();
+    auto const &array_size_pairs =
+      options.get_list_option("associated-array-sizes");
+    for(auto const &array_size_pair : array_size_pairs)
+    {
+      std::string array_name;
+      std::string size_name;
+      try
+      {
+        split_string(array_size_pair, ':', array_name, size_name);
+      }
+      catch(const deserialization_exceptiont &e)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "can't parse parameter value",
+          "--associated-array-sizes",
+          "pairs of array/size parameter names, separated by a ':' colon"};
+      }
+      auto const mapping_insert_result =
+        array_name_to_associated_array_size_variable.insert(
+          {irep_idt{array_name}, irep_idt{size_name}});
+      if(!mapping_insert_result.second)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "duplicate associated size entries for array `" + array_name +
+            "', existing: `" + id2string(mapping_insert_result.first->second) +
+            "', tried to insert: `" + size_name + "'",
+          "--associated-array-sizes"};
+      }
+      auto const size_name_insert_result =
+        variables_that_hold_array_sizes.insert(irep_idt{size_name});
+      if(!size_name_insert_result.second)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "using size parameter `" + size_name + "' more than once",
+          "--associated-array-sizes"};
+      }
+    }
+  }
+}
+
+bool c_object_factory_parameterst::is_array_size_parameter(irep_idt id) const
+{
+  return variables_that_hold_array_sizes.find(id) !=
+         end(variables_that_hold_array_sizes);
+}
+
+optionalt<irep_idt> c_object_factory_parameterst::get_associated_size_variable(
+  irep_idt array_id) const
+{
+  return optional_lookup(
+    array_name_to_associated_array_size_variable, array_id);
+}
+
+bool c_object_factory_parameterst::should_be_treated_as_array(irep_idt id) const
+{
+  return pointers_to_treat_as_array.find(id) !=
+         pointers_to_treat_as_array.end();
 }
diff --git a/src/ansi-c/c_object_factory_parameters.h b/src/ansi-c/c_object_factory_parameters.h
index 1da85f407ec..cc338bd830c 100644
--- a/src/ansi-c/c_object_factory_parameters.h
+++ b/src/ansi-c/c_object_factory_parameters.h
@@ -9,7 +9,11 @@ Author: Daniel Poetzl
 #ifndef CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H
 #define CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H
 
+#include <map>
+#include <set>
 #include <util/object_factory_parameters.h>
+#include <util/optional.h>
+#include <util/options.h>
 
 struct c_object_factory_parameterst final : public object_factory_parameterst
 {
@@ -21,6 +25,19 @@ struct c_object_factory_parameterst final : public object_factory_parameterst
     : object_factory_parameterst(options)
   {
   }
+
+  bool should_be_treated_as_array(irep_idt id) const;
+  bool is_array_size_parameter(irep_idt id) const;
+  optionalt<irep_idt> get_associated_size_variable(irep_idt array_id) const;
+
+  void set(const optionst &options) override;
+
+  std::size_t max_dynamic_array_size = 2;
+
+private:
+  std::set<irep_idt> pointers_to_treat_as_array;
+  std::set<irep_idt> variables_that_hold_array_sizes;
+  std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
 };
 
 /// Parse the c object factory parameters from a given command line
diff --git a/src/util/object_factory_parameters.h b/src/util/object_factory_parameters.h
index 1904205ff30..8f52e42e9e6 100644
--- a/src/util/object_factory_parameters.h
+++ b/src/util/object_factory_parameters.h
@@ -77,7 +77,7 @@ struct object_factory_parameterst
   irep_idt function_id;
 
   /// Assigns the parameters from given options
-  void set(const optionst &);
+  virtual void set(const optionst &);
 };
 
 void parse_object_factory_options(const cmdlinet &, optionst &);