Skip to content

Commit 293ceff

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 ed7f7ec commit 293ceff

File tree

1 file changed

+7
-19
lines changed

1 file changed

+7
-19
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 7 additions & 19 deletions
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)