Adding test to ensure methods on return type of opaque function

These methods should be loaded for all classes where an instance might
be seen and the return of an opaque method is one such instance.

Author: thk123

jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class

@@ -0,0 +1,7 @@
+public class Bar {
+  public int x;
+
+  public void cproverNondetInitialize() {
+
+  }
+}

jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java

@@ -0,0 +1,5 @@
+public class Baz {
+  public void cproverNondetInitialize() {
+
+  }
+}

jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class

@@ -0,0 +1,11 @@
+public class Foo {
+  public Bar subType;
+
+  public Baz[] arraySubtype;
+
+  public Gen<GenFiller> genSubtype;
+
+  public void cproverNondetInitialize() {
+
+  }
+}

jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.java

@@ -0,0 +1,3 @@
+public class Gen<T> {
+  T t;
+}

jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.class

@@ -0,0 +1,7 @@
+public class GenFiller {
+  public int i;
+
+  public void cproverNondetInitialize() {
+
+  }
+

jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java

@@ -0,0 +1,6 @@
+public class Opaque
+{
+  static Foo opaqueMethod() {
+    return null;
+  }
+}

jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class

@@ -0,0 +1,5 @@
+public class TestClass {
+  public static void testFunction() {
+    int x = Opaque.opaqueMethod().subType.x;
+  }
+}

jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java

@@ -0,0 +1,12 @@
+CORE
+TestClass.class
+--function TestClass.testFunction --lazy-methods --verbosity 10
+CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V
+CI lazy methods: elaborate java::Bar\.cproverNondetInitialize:\(\)V
+CI lazy methods: elaborate java::Baz\.cproverNondetInitialize:\(\)V
+CI lazy methods: elaborate java::GenFiller\.cproverNondetInitialize:\(\)V
+--
+--
+Testing that the return type of an opaque method is correctly elaborated. The
+cproverNondetInitialize should be loaded for all classes where an instance might
+be seen.