Add classes to needed classes for parameters and returns for opaque calls

Use gather all fields when setting up the return of an opaque method

This can be considered an input to the function under test, so therefore
we need to set it up in the same way.

Author: thk123

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -177,17 +177,6 @@ bool ci_lazy_methodst::operator()(
       symbol_table);
   }
 
-  // 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

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1038,6 +1038,16 @@ bool java_bytecode_languaget::convert_single_method(
     return false;
   }
 
+  // The return of an opaque function is a source of an otherwise invisible
+  // instantiation, so here we ensure we've loaded the appropriate classes.
+  const code_typet function_type = to_code_type(symbol.type);
+  if(
+    const pointer_typet *pointer_return_type =
+      type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
+  {
+    needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
+  }
+
   return true;
 }