Merge pull request #2335 from thk123/bugfix/load-classes-from-opaque-calls

Load classes from opaque calls [TG-3657]

Author: Thomas Kiley

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() {
+
+  }
+