Add test exercising static, virtual and interface lambdas

These compile down to direct references to a static, virtual and interface method (i.e. to
method reference kinds REF_invokeStatic, REF_invokeVirtual and REF_invokeInterface as described
at https://docs.oracle.com/javase/9/docs/api/java/lang/invoke/MethodHandleInfo.html)

Author: smowton

jbmc/regression/jbmc/lambda-reference-kinds/IntToInt.class

@@ -0,0 +1,3 @@
+interface IntToInt {
+  public int f(int x);
+}

jbmc/regression/jbmc/lambda-reference-kinds/IntToInt.java

@@ -0,0 +1,5 @@
+interface OtherInterface {
+
+  int f(int x);
+
+}

jbmc/regression/jbmc/lambda-reference-kinds/OtherInterface.class

@@ -0,0 +1,30 @@
+public class Test implements OtherInterface {
+
+  public static int staticMethod(int x) { return x + 1; }
+
+  private int field = 1;
+
+  public int instanceMethod(int x) { return field + x; }
+
+  // Implement OtherInterface
+  public int f(int x) { return x + 1; }
+
+  interface MakeTest {
+    public Test makeTest();
+  }
+
+  public static void main() {
+
+    IntToInt staticMethodBound = Test::staticMethod;
+    Test instance = new Test();
+    IntToInt instanceMethodBound = instance::instanceMethod;
+    IntToInt interfaceMethodBound = ((OtherInterface)instance)::f;
+    MakeTest makeTest = Test::new;
+
+    assert staticMethodBound.f(1) == 2;
+    assert interfaceMethodBound.f(1) == 2;
+    assert instanceMethodBound.f(1) == 2;
+    assert makeTest.makeTest().instanceMethod(1) == 2;
+
+  }
+}

jbmc/regression/jbmc/lambda-reference-kinds/OtherInterface.java

@@ -0,0 +1,15 @@
+CORE
+Test
+--function Test.main
+^VERIFICATION SUCCESSFUL$
+line 24 assertion at file Test\.java line 24 function java::Test\.main:\(\)V bytecode-index 30: SUCCESS
+line 25 assertion at file Test\.java line 25 function java::Test\.main:\(\)V bytecode-index 41: SUCCESS
+line 26 assertion at file Test\.java line 26 function java::Test\.main:\(\)V bytecode-index 52: SUCCESS
+line 27 assertion at file Test\.java line 27 function java::Test\.main:\(\)V bytecode-index 64: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that the REF_invokeStatic, REF_invokeDynamic, REF_newInvokeSpecial and REF_invokeInterface method
+handles present in Test.class behave as intended. REF_invokeSpecial is used for the synthetic lambda methods
+(and private method calls), and is exercised in other lambda tests.

jbmc/regression/jbmc/lambda-reference-kinds/Test$MakeTest.class

@@ -121,7 +121,7 @@ static optionalt<irep_idt> get_unique_abstract_method(
     }
     if(!ns.lookup(mangled_name).type.get_bool(ID_C_abstract))
       continue;
-    if(result.has_value() && mangled_name != *result)
+    if(result.has_value())
     {
       throw no_unique_unimplemented_method_exceptiont(
         "produces a type with at least two unimplemented methods");