Fix for crashing lambdas in a package [TG-2478]

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);
+  }
+}

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.

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;