From 7366fda6b17223b96b2f06fb3ebd9ebd2dc08708 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Wed, 28 Mar 2018 11:39:57 +0100
Subject: [PATCH 1/2] Format class name for lambda method handles

---
 src/java_bytecode/java_bytecode_parser.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

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;

From 7d4441d91bc0daac10f8a185dd8bf6d5d31ca3a6 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Wed, 28 Mar 2018 11:52:15 +0100
Subject: [PATCH 2/2] Regression test for lambda in a package

---
 .../cbmc-java/lambda3/LambdaTest/Lamb1.class    | Bin 0 -> 164 bytes
 .../cbmc-java/lambda3/LambdaTest/Test.class     | Bin 0 -> 1444 bytes
 .../cbmc-java/lambda3/LambdaTest/Test.java      |  16 ++++++++++++++++
 regression/cbmc-java/lambda3/test.desc          |   8 ++++++++
 4 files changed, 24 insertions(+)
 create mode 100644 regression/cbmc-java/lambda3/LambdaTest/Lamb1.class
 create mode 100644 regression/cbmc-java/lambda3/LambdaTest/Test.class
 create mode 100644 regression/cbmc-java/lambda3/LambdaTest/Test.java
 create mode 100644 regression/cbmc-java/lambda3/test.desc

diff --git a/regression/cbmc-java/lambda3/LambdaTest/Lamb1.class b/regression/cbmc-java/lambda3/LambdaTest/Lamb1.class
new file mode 100644
index 0000000000000000000000000000000000000000..d247ec682509d5c53f5f996315d3cd8e48b2acf6
GIT binary patch
literal 164
zcmX^0Z`VEs1_l!bPId-%b_Nbc2F{$s+$6WsyktX01`Q3Lti-ZJ{hY+SbbZgflGOCn
zB5O@7VvG!2!TF^{$*FFcIjKN1LQ;!M^gvn}83cTQ=A|TpMD#&Sps@l7L;aJoQj<&A
c7#J8Cn1Jp8(kzS&%nU3b76U7gWMW_g02Wm!*Z=?k

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/lambda3/LambdaTest/Test.class b/regression/cbmc-java/lambda3/LambdaTest/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..8049c1fbea38030cd81d5055a9a4688308bfdf50
GIT binary patch
literal 1444
zcmbVMOH<QO6#gzP4Wxk<P{bEjELz%1LGeWqRAv}E)54+*Gw!@?FAzwRPLg)OUxgbV
zEL^g1{7H`Exk<(bjf~?WIp?07$9KN_O}_p({Q_VKFI6bGIZpme5_gbQF^jwMbx%P~
z!5l+kMK^VKl_8d!+hK^WTP?wms_LfL?6w=i-sTO1BI8x7$&DRu>+&1~<L<uhFpO2J
zyxnN=ZQ-~j`6@H0wrKYJFhe<4J>WfFGPt={s+g|W6LvWwG#3$LV8;v-(O=#XVx!$y
zl=wmzq`OEUM(Qqa9@cor!>b@qjSLTJwhu46z_9s`03%TR1@jS6P`A2vQ*7vxzhTMC
zyktSc5QZ7juPn=TT$^`l!rix8PAY*y8bvbqHO!+#aHTCOSkSPD2O1t?NnXu)uBlU>
z+pWfdXu1>%C3$41c!b9cxu`v(Hc*kk6GAQ7+US~1Vt6^KHj<Fvhto}r^)Uwb&oHE$
z?hZG)#14tC!l3lzX=|5ZGFOR0rQoTCXLzn*3Rf9s`b~ASXB~=?KbZ*SyS(XIHYq3B
z?w=H_k>abCb=d7NXcf~G_PW6xN05rYh4%~k`B(Frn=L~)S-&tW+`4P)=3Y2*u5kOf
zBmVEBKl0+*FhjxEb#54S-4$g8FBoS3;3sMyhUts*kRdTB^bY}I^pJW%;wG;|mXRII
ze*}9^&H$41PIy5D8u^-^fDw$+X&5P_DI$xHC|kD6<O`?dqE<XZs&Iy6G5;B{0h|;I
zzNMU)*LNIo@>K$mq%Kkequz{+-v?umKRW7&3Gzr^lyM1{sre*DhrqsLO2L)1D%BI9
zs0Aoe`45N}=z04IgKuglR1jW94Gl{D8k7nKf!4Z4BjrNZy~-O{A*<4mWvrr1<EH5>
M$+$&18QezZC(g-c9RL6T

literal 0
HcmV?d00001

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.