Skip to content

Commit 3476187

Browse files
committed
Protect needed_lazy_methods access in an if-block
If we are not using CI lazy methods here (as could happen after the change from the previous commit that makes sure convert_single_method is run for all methods), needed_lazy_methods is an empty optional and we cannot access it.
1 parent a57ddfc commit 3476187

File tree

1 file changed

+20
-17
lines changed

1 file changed

+20
-17
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 20 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1312,24 +1312,27 @@ bool java_bytecode_languaget::convert_single_method(
13121312
return false;
13131313
}
13141314

1315-
// The return of an opaque function is a source of an otherwise invisible
1316-
// instantiation, so here we ensure we've loaded the appropriate classes.
1317-
const java_method_typet function_type = to_java_method_type(symbol.type);
1318-
if(
1319-
const pointer_typet *pointer_return_type =
1320-
type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1315+
if(needed_lazy_methods)
13211316
{
1322-
// If the return type is abstract, we won't forcibly instantiate it here
1323-
// otherwise this can cause abstract methods to be explictly called
1324-
// TODO(tkiley): Arguably no abstract class should ever be added to
1325-
// TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1326-
// TODO(tkiley): investigation
1327-
namespacet ns{symbol_table};
1328-
const java_class_typet &underlying_type =
1329-
to_java_class_type(ns.follow(pointer_return_type->subtype()));
1330-
1331-
if(!underlying_type.is_abstract())
1332-
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1317+
// The return of an opaque function is a source of an otherwise invisible
1318+
// instantiation, so here we ensure we've loaded the appropriate classes.
1319+
const java_method_typet function_type = to_java_method_type(symbol.type);
1320+
if(
1321+
const pointer_typet *pointer_return_type =
1322+
type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1323+
{
1324+
// If the return type is abstract, we won't forcibly instantiate it here
1325+
// otherwise this can cause abstract methods to be explictly called
1326+
// TODO(tkiley): Arguably no abstract class should ever be added to
1327+
// TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1328+
// TODO(tkiley): investigation
1329+
namespacet ns{symbol_table};
1330+
const java_class_typet &underlying_type =
1331+
to_java_class_type(ns.follow(pointer_return_type->subtype()));
1332+
1333+
if(!underlying_type.is_abstract())
1334+
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1335+
}
13331336
}
13341337

13351338
INVARIANT(declaring_class(symbol), "Method must have a declaring class.");

0 commit comments

Comments
 (0)