!fixup se gather all fields when setting up the return of an opaque m

thk123 · thk123 · commit a2e928689c8f · 2018-06-12T13:49:38.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -1039,6 +1039,8 @@ 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 =

Original file line number	Diff line number	Diff line change
`@@ -1039,6 +1039,8 @@ bool java_bytecode_languaget::convert_single_method(`
`1039`	`1039`	`return false;`
`1040`	`1040`	`}`
`1041`	`1041`
	`1042`	`+ // The return of an opaque function is a source of an otherwise invisible`
	`1043`	`+ // instantiation, so here we ensure we've loaded the appropriate classes.`
`1042`	`1044`	`const code_typet function_type = to_code_type(symbol.type);`
`1043`	`1045`	`if(`
`1044`	`1046`	`const pointer_typet *pointer_return_type =`