Add test verifying that the cproverNondetInitialize method is always …

…loaded

Test is disabled because of test-runner problems described in the
following issue: diffblue#2267

jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java

@@ -0,0 +1,11 @@
+import org.cprover.CProver;
+
+class ObjectWithNondetInitialize {
+  private int value_;
+  public void cproverNondetInitialize() {
+    CProver.assume(value_ == 13);
+  }
+  public int value() {
+    return value_;
+  }
+}

jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java

@@ -0,0 +1,7 @@
+import org.cprover.CProver;
+
+public class Opaque {
+  public ObjectWithNondetInitialize get() {
+    return new ObjectWithNondetInitialize();
+  }
+}

jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.java

@@ -0,0 +1,5 @@
+public class Test {
+  public int test() {
+    return (new Opaque()).get().value();
+  }
+}

jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+Test.class
+--function Test.test --show-goto-functions --lazy-methods
+EXIT=0
+SIGNAL=0
+ObjectWithNondetInitialize\.cproverNondetInitialize\(\)
+--
+--
+Check if cproverNondetInitialize method is loaded in an object
+returned from an opaque method
+https://github.com/diffblue/cbmc/issues/2273