Merge pull request #1769 from smowton/smowton/fix/nondet-initialize-after-initialize

Java frontend: only run cproverNondetInitialize after all fields are initialized

Author: smowton

regression/cbmc-java/NondetInitValidate/Test.class renamed to regression/cbmc-java/NondetInit/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/NondetInitValidate/Test.java renamed to regression/cbmc-java/NondetInit/Test.java

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

regression/cbmc-java/NondetInitValidate/test.desc renamed to regression/cbmc-java/NondetInit/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/NondetInitValidate/test_lazy.desc renamed to regression/cbmc-java/NondetInit/test_lazy.desc

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

regression/cbmc-java/NondetInit2/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;