Merge pull request #1660 from smowton/smowton/fix/lazy_methods_array_parameters

TG-1877: Include array pointer types in needed classes

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); }
+
+}