diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class new file mode 100644 index 00000000000..ee136a7e1c3 Binary files /dev/null and b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class differ diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java new file mode 100644 index 00000000000..e9660b876cb --- /dev/null +++ b/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_; + } +} diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java new file mode 100644 index 00000000000..616c1ff6bb2 --- /dev/null +++ b/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(); + } +} diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class new file mode 100644 index 00000000000..a809eb786c4 Binary files /dev/null and b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class differ diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.java b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.java new file mode 100644 index 00000000000..f9c9e77e98d --- /dev/null +++ b/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(); + } +} diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc new file mode 100644 index 00000000000..66e55f3e8d7 --- /dev/null +++ b/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 diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 413f8b3c709..667447bc983 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -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