Split up gen_nondet_init function

Broke up the code handling initilising a pointer into a standalone
function.

Author: thk123

src/java_bytecode/java_object_factory.cpp

@@ -110,6 +110,14 @@ class java_object_factoryt
     bool create_dynamic_objects,
     bool override=false,
     const typet &override_type=empty_typet());
+
+private:
+  void gen_nondet_pointer_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    const irep_idt &class_identifier,
+    bool create_dynamic_objects,
+    const pointer_typet &pointer_type);
 };
 
 /// \param assignments: The code block to add code to
@@ -250,6 +258,74 @@ void java_object_factoryt::gen_pointer_target_init(
   }
 }
 
+/// Initialises a primitive or object tree rooted at `expr`, of type pointer. It
+/// allocates child objects as necessary and nondet-initialising their members,
+/// \param assignments - the code block we are building with
+///   initilisation code
+/// \param expr: lvalue expression to initialise
+/// \param class_identifier - the name of the class so we can identify
+/// special cases where a null pointer is not applicable.
+/// \param create_dynamic_objects: if true, use malloc to allocate objects;
+///   otherwise generate fresh static symbols.
+/// \param pointer_type - The type of the pointer we are initalising
+void java_object_factoryt::gen_nondet_pointer_init(
+  code_blockt &assignments,
+  const exprt &expr,
+  const irep_idt &class_identifier,
+  bool create_dynamic_objects,
+  const pointer_typet &pointer_type)
+{
+  const typet &subtype=ns.follow(pointer_type.subtype());
+
+  if(subtype.id()==ID_struct)
+  {
+    const struct_typet &struct_type=to_struct_type(subtype);
+    const irep_idt struct_tag=struct_type.get_tag();
+    // set to null if found in recursion set and not a sub-type
+    if(recursion_set.find(struct_tag)!=recursion_set.end() &&
+       struct_tag==class_identifier)
+    {
+      assignments.copy_to_operands(
+        get_null_assignment(expr, pointer_type));
+      return;
+    }
+  }
+
+  code_blockt non_null_inst;
+  gen_pointer_target_init(
+    non_null_inst,
+    expr,
+    subtype,
+    create_dynamic_objects);
+
+  if(assume_non_null)
+  {
+    // Add the following code to assignments:
+    // <expr> = <aoe>;
+    assignments.append(non_null_inst);
+  }
+  else
+  {
+    // if(NONDET(_Bool)
+    // {
+    //    <expr> = <null pointer>
+    // }
+    // else
+    // {
+    //    <code from recursive call to gen_nondet_init() with
+    //             tmp$<temporary_counter>>
+    // }
+    auto set_null_inst=get_null_assignment(expr, pointer_type);
+
+    code_ifthenelset null_check;
+    null_check.cond()=side_effect_expr_nondett(bool_typet());
+    null_check.then_case()=set_null_inst;
+    null_check.else_case()=non_null_inst;
+
+    assignments.add(null_check);
+  }
+}
+
 /// Creates a nondet for expr, including calling itself recursively to make
 /// appropriate symbols to point to if expr is a pointer or struct
 /// \param expr: The expression which we are generating a non-determinate value
@@ -277,54 +353,12 @@ void java_object_factoryt::gen_nondet_init(
   {
     // dereferenced type
     const pointer_typet &pointer_type=to_pointer_type(type);
-    const typet &subtype=ns.follow(pointer_type.subtype());
-
-    if(subtype.id()==ID_struct)
-    {
-      const struct_typet &struct_type=to_struct_type(subtype);
-      const irep_idt struct_tag=struct_type.get_tag();
-      // set to null if found in recursion set and not a sub-type
-      if(recursion_set.find(struct_tag)!=recursion_set.end() &&
-         struct_tag==class_identifier)
-      {
-        assignments.copy_to_operands(
-          get_null_assignment(expr, pointer_type));
-        return;
-      }
-    }
-
-    code_blockt non_null_inst;
-    gen_pointer_target_init(
-      non_null_inst,
+    gen_nondet_pointer_init(
+      assignments,
       expr,
-      subtype,
-      create_dynamic_objects);
-
-    if(assume_non_null)
-    {
-      // Add the following code to assignments:
-      // <expr> = <aoe>;
-      assignments.append(non_null_inst);
-    }
-    else
-    {
-      // Add the following code to assignments:
-      //           IF !NONDET(_Bool) THEN GOTO <label1>
-      //           <expr> = <null pointer>
-      //           GOTO <label2>
-      // <label1>: <expr> = &tmp$<temporary_counter>;
-      //           <code from recursive call to gen_nondet_init() with
-      //             tmp$<temporary_counter>>
-      // And the next line is labelled label2
-      auto set_null_inst=get_null_assignment(expr, pointer_type);
-
-      code_ifthenelset null_check;
-      null_check.cond()=side_effect_expr_nondett(bool_typet());
-      null_check.then_case()=set_null_inst;
-      null_check.else_case()=non_null_inst;
-
-      assignments.add(null_check);
-    }
+      class_identifier,
+      create_dynamic_objects,
+      pointer_type);
   }
   else if(type.id()==ID_struct)
   {