Use allocate_objectst in the c nondet object factory

Author: danpoe

regression/cbmc/pointer-function-parameters-2/test.desc

@@ -3,10 +3,10 @@ main.c
 --function fun --cover branch
 ^\*\* 7 of 7 covered \(100.0%\)$
 ^Test suite:$
-^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$
-^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
-^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
-^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
+^a=\(\(signed int \*\*\)NULL\), tmp_object_factory(\$\d+)?=[^,]*, tmp_object_factory(\$\d+)?=[^,]*$
+^a=&tmp_object_factory(\$\d+)?!0, tmp_object_factory(\$\d+)?=\(\(signed int \*\)NULL\), tmp_object_factory(\$\d+)?=[^,]*$
+^a=&tmp_object_factory(\$\d+)?!0, tmp_object_factory(\$\d+)?=&tmp_object_factory\$\d+!0, tmp_object_factory(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
+^a=&tmp_object_factory(\$\d+)?!0, tmp_object_factory(\$\d+)?=&tmp_object_factory(\$\d+)?!0, tmp_object_factory(\$\d+)?=4$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/pointer-function-parameters/test.desc

@@ -3,9 +3,9 @@ main.c
 --function fun --cover branch
 ^\*\* 5 of 5 covered \(100\.0%\)$
 ^Test suite:$
-^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
-^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
-^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$
+^a=\(\(signed int \*\)NULL\), tmp_object_factory(\$\d+)?=[^,]*$
+^a=&tmp_object_factory(\$\d+)?!0, tmp_object_factory(\$\d+)?=4$
+^a=&tmp_object_factory(\$\d+)?!0, tmp_object_factory(\$\d+)?=([012356789][0-9]*|4[0-9]+)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -13,6 +13,7 @@ Author: Diffblue Ltd.
 
 #include <ansi-c/c_object_factory_parameters.h>
 
+#include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
@@ -47,62 +48,13 @@ class symbol_factoryt
       object_factory_params(object_factory_params)
   {}
 
-  exprt allocate_object(
-    code_blockt &assignments,
-    const exprt &target_expr,
-    const typet &allocate_type,
-    const bool static_lifetime);
-
   void gen_nondet_init(
     code_blockt &assignments,
     const exprt &expr,
     const std::size_t depth = 0,
     recursion_sett recursion_set = recursion_sett());
 };
 
-/// Create a symbol for a pointer to point to
-/// \param assignments: The code block to add code to
-/// \param target_expr: The expression which we are allocating a symbol for
-/// \param allocate_type: The type to use for the symbol. If this doesn't match
-///   target_expr then a cast will be used for the assignment
-/// \param static_lifetime: Whether the symbol created should have static
-///   lifetime
-/// \return Returns the address of the allocated symbol
-exprt symbol_factoryt::allocate_object(
-  code_blockt &assignments,
-  const exprt &target_expr,
-  const typet &allocate_type,
-  const bool static_lifetime)
-{
-  symbolt &aux_symbol = get_fresh_aux_symbol(
-    allocate_type,
-    id2string(loc.get_function()),
-    "tmp",
-    loc,
-    ID_C,
-    symbol_table);
-  aux_symbol.is_static_lifetime = static_lifetime;
-  symbols_created.push_back(&aux_symbol);
-
-  const typet &allocate_type_resolved=ns.follow(allocate_type);
-  const typet &target_type=ns.follow(target_expr.type().subtype());
-  bool cast_needed=allocate_type_resolved!=target_type;
-
-  exprt aoe=address_of_exprt(aux_symbol.symbol_expr());
-  if(cast_needed)
-  {
-    aoe=typecast_exprt(aoe, target_expr.type());
-  }
-
-  // Add the following code to assignments:
-  //   <target_expr> = &tmp$<temporary_counter>
-  code_assignt assign(target_expr, aoe);
-  assign.add_source_location()=loc;
-  assignments.add(std::move(assign));
-
-  return aoe;
-}
-
 /// 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
@@ -142,7 +94,11 @@ void symbol_factoryt::gen_nondet_init(
 
     code_blockt non_null_inst;
 
-    exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
+    allocate_objectst allocate_objects(
+      ID_C, loc, loc.get_function(), symbol_table);
+
+    exprt allocated = allocate_objects.allocate_non_dynamic_object(
+      non_null_inst, expr, subtype, false, symbols_created);
 
     exprt init_expr;
     if(allocated.id()==ID_address_of)