TG-1877: Include array pointer types in needed classes

Lazy methods attempts a pointer graph walk starting from the main function's
parameters to determine what classes may exist before the main function is
entered; for example, starting at f(A a) implies that an A instance may exist,
and if A itself has a B field that too might exist, and so on. However, until
now this failed to account for array-typed parameters and fields. This commit
amends gather_field_types to account for this special case.

This also adds a test for the generic parameter case, which is not solved yet.

Author: smowton

regression/cbmc-java/lazyloading_array_parameter/asserthere.class

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

regression/cbmc-java/lazyloading_array_parameter/test.class

@@ -0,0 +1,22 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(test[] args) {
+
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}

regression/cbmc-java/lazyloading_array_parameter/test.desc

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

regression/cbmc-java/lazyloading_array_parameter/test.java

@@ -0,0 +1,29 @@
+
+public class test {
+
+  public int f() { return 1; }
+
+  public static void g(container c) {
+
+    if(c == null)
+      return;
+    test[] args = c.test_array;
+    if(args == null || args.length != 1 || args[0] == null)
+      return;
+    asserthere.doassert(args[0].f() == 1);
+
+  }
+
+}
+
+class container {
+  public test[] test_array;
+}
+
+class asserthere {
+
+  // Used to avoid lazy-loading currently marking any class with an
+  // $assertionsEnabled member (i.e. any class that asserts) as needed.
+  public static void doassert(boolean condition) { assert(condition); }
+
+}