Merge pull request #2267 from LAJW/lajw/always-load-cprover-nondet-initialize

[TG-3657] Always load CProver.nondetInitialize

Author: romainbrenguier

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

@@ -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/ObjectWithNondetInitialize.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/Opaque.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.class

@@ -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

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

@@ -248,6 +248,17 @@ bool ci_lazy_methodst::operator()(
     }
   }
 
+  // cproverNondetInitialize has to be force-loaded for mocks to return valid
+  // objects (objects which satisfy invariants specified in the
+  // cproverNondetInitialize method)
+  for(const auto &class_name : instantiated_classes)
+  {
+    const irep_idt cprover_validate =
+      id2string(class_name) + ".cproverNondetInitialize:()V";
+    if(symbol_table.symbols.count(cprover_validate))
+      methods_already_populated.insert(cprover_validate);
+  }
+
   // Remove symbols for methods that were declared but never used:
   symbol_tablet keep_symbols;
   // Manually keep @inflight_exception, as it is unused at this stage