diff --git a/regression/cbmc-java/lambda2/SymStream.class b/regression/cbmc-java/lambda2/SymStream.class new file mode 100644 index 00000000000..a473c854861 Binary files /dev/null and b/regression/cbmc-java/lambda2/SymStream.class differ diff --git a/regression/cbmc-java/lambda2/readme.txt b/regression/cbmc-java/lambda2/readme.txt new file mode 100644 index 00000000000..38647bdebb1 --- /dev/null +++ b/regression/cbmc-java/lambda2/readme.txt @@ -0,0 +1 @@ +from https://github.com/symphonyoss/symphony-java-client/ diff --git a/regression/cbmc-java/lambda2/test.desc b/regression/cbmc-java/lambda2/test.desc new file mode 100644 index 00000000000..2127f00ead7 --- /dev/null +++ b/regression/cbmc-java/lambda2/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +SymStream.class +--verbosity 10 --show-goto-functions +lambda function reference org/symphonyoss/symphony/clients/model/SymUser\.toSymUser in class \"SymStream\" +^EXIT=0 +^SIGNAL=0 +-- +-- +lambda functions without "lambda$" prefix aren't recognized currently TG-2691 diff --git a/regression/cbmc-java/lambda2/test_no_crash.desc b/regression/cbmc-java/lambda2/test_no_crash.desc new file mode 100644 index 00000000000..933732babea --- /dev/null +++ b/regression/cbmc-java/lambda2/test_no_crash.desc @@ -0,0 +1,8 @@ +CORE +SymStream.class +--verbosity 10 --show-goto-functions +^EXIT=0 +^SIGNAL=0 +-- +-- +just to test that it doesn't crash in this situation, cf. TG-2684 diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index cce0f95a89c..d4eb82002c0 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1893,10 +1893,18 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) optionalt lambda_method_handle = parse_method_handle(method_handle_infot{method_handle_argument}); - if( - !lambda_method_handle.has_value() || + if(!lambda_method_handle.has_value()) + { + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(u2_values); + parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = + lambda_method_handle; + return; + } + else if( lambda_method_handle->handle_type != - method_handle_typet::LAMBDA_METHOD_HANDLE) + method_handle_typet::LAMBDA_METHOD_HANDLE) { lambda_method_handle->u2_values = std::move(u2_values); error() << "ERROR: could not parse lambda function method handle"