Java: run nondet-initialize method *after* initialization

Previously this method was run after each supertype of a relevant type
was initialised, e.g. if MyClass <: MySupertype <: Object, then
MyClass.cproverNondetInitialize would get run after my inner Object was
set up, then again after MySupertype was set up, then one more time after
the whole class was set up. Now it will only run after the whole initialisation
is complete.

This fixes a bug where array members could have inconsistent length and data field
values because they had not been initialised yet, leading to an assertion failure
during nondetInitialize, and also has the desirable side-effect that an initialiser
will still be run when creating a subtype.

Author: smowton

regression/cbmc-java/NondetInit2/Test.class

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Test nondetInput) {
+    }
+
+}

regression/cbmc-java/NondetInit2/Test.java

@@ -0,0 +1,5 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+

regression/cbmc-java/NondetInit2/test.desc

@@ -0,0 +1,22 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Subclass nondetInput) {
+        // The condition enforced by cproverNondetInitialize should hold
+        // even though the parameter is a subtype of Test, not directly an
+        // instance of Test itself.
+        assert nondetInput.arr.length == 1;
+    }
+
+}
+
+class Subclass extends Test { }

regression/cbmc-java/NondetInit3/Subclass.class

@@ -0,0 +1,5 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+

regression/cbmc-java/NondetInit3/Test.class

@@ -1076,16 +1076,16 @@ void java_object_factoryt::gen_nondet_struct_init(
     }
   }
 
-  // If <class_identifier>.cproverValidate() can be found in the
+  // If <class_identifier>.cproverNondetInitialize() can be found in the
   // symbol table, we add a call:
   // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // expr.cproverValidate();
+  // expr.cproverNondetInitialize();
   // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-  const irep_idt validate_method_name =
-    "java::" + id2string(class_identifier) + ".cproverNondetInitialize:()V";
+  const irep_idt init_method_name =
+    "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
 
-  if(const auto func = symbol_table.lookup(validate_method_name))
+  if(const auto func = symbol_table.lookup(init_method_name))
   {
     const code_typet &type = to_code_type(func->type);
     code_function_callt fun_call;