diff --git a/regression/cbmc-java/lambda3/LambdaTest/Lamb1.class b/regression/cbmc-java/lambda3/LambdaTest/Lamb1.class new file mode 100644 index 00000000000..d247ec68250 Binary files /dev/null and b/regression/cbmc-java/lambda3/LambdaTest/Lamb1.class differ diff --git a/regression/cbmc-java/lambda3/LambdaTest/Test.class b/regression/cbmc-java/lambda3/LambdaTest/Test.class new file mode 100644 index 00000000000..8049c1fbea3 Binary files /dev/null and b/regression/cbmc-java/lambda3/LambdaTest/Test.class differ diff --git a/regression/cbmc-java/lambda3/LambdaTest/Test.java b/regression/cbmc-java/lambda3/LambdaTest/Test.java new file mode 100644 index 00000000000..3361a9bd436 --- /dev/null +++ b/regression/cbmc-java/lambda3/LambdaTest/Test.java @@ -0,0 +1,16 @@ +package LambdaTest; + +interface Lamb1 { + public Integer lambFunc1(Integer x); +} + +class Test { + + public static Integer recvLambda(Integer y, Integer z) { + Lamb1 lmb1 = (x) -> x = y + z; // Initializing in a lambda statement + if (lmb1 != null && z != null) { + return lmb1.lambFunc1(y); + } + return lmb1.lambFunc1(z); + } +} diff --git a/regression/cbmc-java/lambda3/test.desc b/regression/cbmc-java/lambda3/test.desc new file mode 100644 index 00000000000..a025de30ffd --- /dev/null +++ b/regression/cbmc-java/lambda3/test.desc @@ -0,0 +1,8 @@ +CORE +LambdaTest/Test.class +--show-symbol-table --function LambdaTest.Test.recvLambda +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This is to verify that parsing lambdas in a package does not crash. diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 46ab444d380..1a0a4d26627 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1777,9 +1777,13 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) const name_and_type_infot &name_and_type = ref_entry.get_name_and_type(pool_entry_lambda); + std::string class_name = class_entry.get_name(pool_entry_lambda); + // replace '.' for '$' (inner classes) + std::replace(class_name.begin(), class_name.end(), '.', '$'); + // replace '/' for '.' (package) + std::replace(class_name.begin(), class_name.end(), '/', '.'); const std::string method_ref = - class_entry.get_name(pool_entry_lambda) + "." + - name_and_type.get_name(pool_entry_lambda) + ':' + + class_name + "." + name_and_type.get_name(pool_entry_lambda) + ':' + name_and_type.get_descriptor(pool_entry_lambda); lambda_method_handlet lambda_method_handle;