Java frontend: handle lambdas that adapt a method with a return type to an interface method returning void

Author: smowton

jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class

@@ -0,0 +1,31 @@
+public class Test {
+
+  public int lastArgument = 0;
+  public int intToInt(int x) { lastArgument = x; return x + 1; }
+  public Integer intToInteger(int x) { lastArgument = x; return x + 1; }
+  public Object intToObject(int x) { lastArgument = x; return -1; }
+
+  public interface IntToVoid {
+    void consume(int x);
+  }
+
+  public static void test() {
+    Test t = new Test();
+
+    IntToVoid intToVoid = t::intToInt;
+    intToVoid.consume(5);
+    assert t.lastArgument == 5;
+
+    IntToVoid intToVoid2 = t::intToInteger;
+    intToVoid2.consume(10);
+    assert t.lastArgument == 10;
+
+    IntToVoid intToVoid3 = t::intToObject;
+    intToVoid3.consume(15);
+    assert t.lastArgument == 15;
+
+    assert false; // Check we got here
+
+  }
+
+}

jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class

@@ -0,0 +1,9 @@
+CORE
+Test
+--function Test.test --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+\[java::Test\.test:\(\)V\.assertion\.1\] line 17 assertion at file Test\.java line 17 function java::Test\.test:\(\)V bytecode-index 22: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.2\] line 21 assertion at file Test\.java line 21 function java::Test\.test:\(\)V bytecode-index 41: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.3\] line 25 assertion at file Test\.java line 25 function java::Test\.test:\(\)V bytecode-index 60: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.4\] line 27 assertion at file Test\.java line 27 function java::Test\.test:\(\)V bytecode-index 66: FAILURE

jbmc/regression/jbmc/lambda-void-return-type/Test$ObjectToVoid.class

@@ -806,7 +806,7 @@ codet invokedynamic_synthetic_method(
       "param" + std::to_string(i));
   }
 
-  if(callee_return_type != empty_typet() && !is_constructor_lambda)
+  if(function_type.return_type() != empty_typet() && !is_constructor_lambda)
   {
     symbol_exprt result_local = create_and_declare_local(
       function_id, "return_value", callee_return_type, symbol_table, result);