Merge pull request #4787 from smowton/smowton/feature/synthesise-lambda-classes

Synthesise lambda classes

Author: Łukasz A.J. Wrona

jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.class

@@ -0,0 +1,6 @@
+interface InterfaceDeclaringEquals {
+
+  public int f(int x);
+
+  public boolean equals(Object other);
+}

jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.java

@@ -0,0 +1,6 @@
+interface InterfaceWithDefaults {
+
+  public int f(int x);
+
+  public default int g() { return 1; }
+}

jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.class

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

jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.java

@@ -0,0 +1 @@
+interface StubSuperinterface extends StubInterface {}

jbmc/regression/jbmc/lambda-unhandled-types/StubInterface.java

@@ -0,0 +1,10 @@
+public class Test {
+
+  public static void main() {
+
+    StubInterface stubInterface = (x -> x);
+    StubSuperinterface stubSuperinterface = (x -> x);
+    InterfaceDeclaringEquals interfaceDeclaringEquals = (x -> x);
+    InterfaceWithDefaults interfaceWithDefaults = (x -> x);
+  }
+}

jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.class

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--function Test.main --verbosity 10
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+^ignoring invokedynamic at java::Test.main:\(\)V address 0 which produces a stub type java::StubInterface
+^ignoring invokedynamic at java::Test.main:\(\)V address 6 which produces type java::StubSuperinterface which should have exactly one abstract method but actually has 0.
+^ignoring invokedynamic at java::Test.main:\(\)V address 12 which produces type java::InterfaceDeclaringEquals which should have exactly one abstract method but actually has 2.
+^ignoring invokedynamic at java::Test.main:\(\)V address 18 which produces type java::InterfaceWithDefaults which should have exactly one abstract method but actually has 2.
+--
+--
+This exercises four cases that aren't currently supported: stub interfaces, stub
+superinterfaces, interfaces that declare methods also declared on
+java.lang.Object, and interfaces that provide default methods. All we require at
+this point is that jbmc shouldn't crash when these are seen.