Skip to content

Commit 33ec445

Browse files
author
thk123
committed
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.
1 parent 0f318dc commit 33ec445

File tree

1 file changed

+7
-19
lines changed

1 file changed

+7
-19
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

+7-19
Original file line numberDiff line numberDiff line change
@@ -1039,25 +1039,13 @@ bool java_bytecode_languaget::convert_single_method(
10391039
return false;
10401040
}
10411041

1042-
const auto type_adder = [&needed_lazy_methods](const typet &type) {
1043-
const pointer_typet *return_type_pointer =
1044-
type_try_dynamic_cast<pointer_typet>(type);
1045-
if(return_type_pointer)
1046-
{
1047-
const symbol_typet *symbol_type =
1048-
type_try_dynamic_cast<symbol_typet>(return_type_pointer->subtype());
1049-
if(symbol_type)
1050-
{
1051-
needed_lazy_methods->add_needed_class(symbol_type->get_identifier());
1052-
}
1053-
}
1054-
};
1055-
1056-
// opaque method, but we should load the classes of the parameters and return??
1057-
const code_typet function_type =to_code_type(symbol.type);
1058-
type_adder(function_type.return_type());
1059-
for(const code_typet::parametert &parameter : function_type.parameters())
1060-
type_adder(parameter.type());
1042+
const code_typet function_type = to_code_type(symbol.type);
1043+
if(
1044+
const pointer_typet *pointer_return_type =
1045+
type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1046+
{
1047+
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1048+
}
10611049

10621050
return true;
10631051
}

0 commit comments

Comments
 (0)