Merge pull request diffblue#1765 from smowton/smowton/fix/ci-lazy-methods-array-element-types

CI lazy methods: re-explore array types with different element types

Author: smowton

regression/cbmc-java/lazyloading_multiple_array_types/A.class

@@ -0,0 +1,7 @@
+public class A {
+
+    public int f() {
+        return 1;
+    }
+
+}

regression/cbmc-java/lazyloading_multiple_array_types/A.java

@@ -0,0 +1,7 @@
+public class B {
+
+    public int g() {
+        return 5;
+    }
+
+}

regression/cbmc-java/lazyloading_multiple_array_types/B.class

@@ -0,0 +1,17 @@
+public class Test {
+  
+  A[] arrayA;
+  B[] arrayB;
+
+  public static void check(Test t) {
+    if (t == null || t.arrayA == null || t.arrayB == null ||
+        t.arrayA.length == 0 || t.arrayB.length == 0 ||
+        t.arrayA[0] == null || t.arrayB[0] == null)
+      return;
+    int i = t.arrayA[0].f();
+    int j = t.arrayB[0].g();
+    int sum = i + j;
+    assert(sum == 6);
+  }
+
+}

regression/cbmc-java/lazyloading_multiple_array_types/B.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--lazy-methods --verbosity 10 --function Test.check
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)I
+elaborate java::B\.g:\(\)I
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading_multiple_array_types/Test.class

@@ -344,7 +344,10 @@ void ci_lazy_methodst::initialize_needed_classes_from_pointer(
   const symbol_typet &class_type=to_symbol_type(pointer_type.subtype());
   const auto &param_classid=class_type.get_identifier();
 
-  if(needed_lazy_methods.add_needed_class(param_classid))
+  // Note here: different arrays may have different element types, so we should
+  // explore again even if we've seen this classid before in the array case.
+  if(needed_lazy_methods.add_needed_class(param_classid) ||
+     is_java_array_tag(param_classid))
   {
     gather_field_types(pointer_type.subtype(), ns, needed_lazy_methods);
   }