Add some documentation to java_object_factory

Add a high-level overview of the recursive algorithm in the file.

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -974,7 +974,7 @@ void java_object_factoryt::gen_nondet_struct_init(
   // Should we write the whole object?
   // * Not if this is a sub-structure (a superclass object), as our caller will
   //   have done this already
-  // * Not if the object has already been initialised by our caller, in whic
+  // * Not if the object has already been initialised by our caller, in which
   //   case they will set `skip_classid`
   // * Not if we're re-initializing an existing object (i.e. update_in_place)
 
@@ -1094,7 +1094,7 @@ void java_object_factoryt::gen_nondet_struct_init(
   }
 }
 
-/// Initializes a primitive-typed or referece-typed object tree rooted at
+/// Initializes a primitive-typed or reference-typed object tree rooted at
 /// `expr`, allocating child objects as necessary and nondet-initializing their
 /// members, or if MUST_UPDATE_IN_PLACE is set, re-initializing
 /// already-allocated objects.

jbmc/src/java_bytecode/java_object_factory.h

@@ -19,16 +19,19 @@ Author: Daniel Kroening, [email protected]
 /// that are called but for which we don't have a body (overapproximating the
 /// return value and possibly side effects).
 ///
-/// The two main APIs are \ref gen_nondet_init() and \ref object_factory(), at
-/// the bottom of the file.  Their purpose is very similar. A call to
+/// The two main APIs are \ref gen_nondet_init() and \ref object_factory()
+/// (which calls gen_nondet_init()), at the bottom of the file.
+/// A call to
 ///
 ///   gen_nondet_init(expr, code, ..., update_in_place)
 ///
 /// appends to `code` (a code_blockt) a sequence of statements that
 /// non-deterministically initialize the `expr` (which is expected to be an
 /// l-value exprt) with a primitive or reference value of type equal to or
 /// compatible with `expr.type()` -- see documentation for the argument
-/// `pointer_type_selector` for additional details.
+/// `pointer_type_selector` for additional details. gen_nondet_init() is the
+/// starting point of a recursive algorithm, and most other functions in this
+/// file are different (recursive or base) cases depending on the type of expr.
 ///
 /// The code generated mainly depends on the parameter `update_in_place`. Assume
 /// that `expr` is a reference to an object (in our IR, that means a pointer to