Java frontend: support lambda method references that imply primitive type widening

For example, an int -> int method is a valid instantiation of a functional interface
that expects a byte -> int, or one that expects an int -> long. In both cases it's down
to the metafactory / our code that emulates its behaviour to add the widening cast.

Author: smowton

jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testByteToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testByteToLong:\(\)V.assertion\.1\] line 26 assertion at file Test\.java line 26 function java::Test\.testByteToLong:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testByteToLong:\(\)V.assertion\.2\] line 27 assertion at file Test\.java line 27 function java::Test\.testByteToLong:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testDoubleToFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testDoubleToFloat:\(\)V.assertion\.1\] line 66 assertion at file Test\.java line 66 function java::Test\.testDoubleToFloat:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testDoubleToFloat:\(\)V.assertion\.2\] line 67 assertion at file Test\.java line 67 function java::Test\.testDoubleToFloat:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testFloatToDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testFloatToDouble:\(\)V.assertion\.1\] line 44 assertion at file Test\.java line 44 function java::Test\.testFloatToDouble:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testFloatToDouble:\(\)V.assertion\.2\] line 45 assertion at file Test\.java line 45 function java::Test\.testFloatToDouble:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testIntToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testIntToLong:\(\)V.assertion\.1\] line 38 assertion at file Test\.java line 38 function java::Test\.testIntToLong:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testIntToLong:\(\)V.assertion\.2\] line 39 assertion at file Test\.java line 39 function java::Test\.testIntToLong:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testLongToByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testLongToByte:\(\)V.assertion\.1\] line 72 assertion at file Test\.java line 72 function java::Test\.testLongToByte:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testLongToByte:\(\)V.assertion\.2\] line 73 assertion at file Test\.java line 73 function java::Test\.testLongToByte:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testLongToInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testLongToInt:\(\)V.assertion\.1\] line 84 assertion at file Test\.java line 84 function java::Test\.testLongToInt:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testLongToInt:\(\)V.assertion\.2\] line 85 assertion at file Test\.java line 85 function java::Test\.testLongToInt:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testLongToShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testLongToShort:\(\)V.assertion\.1\] line 78 assertion at file Test\.java line 78 function java::Test\.testLongToShort:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testLongToShort:\(\)V.assertion\.2\] line 79 assertion at file Test\.java line 79 function java::Test\.testLongToShort:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc

@@ -0,0 +1,7 @@
+CORE
+Test
+--function Test\.testShortToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.testShortToLong:\(\)V.assertion\.1\] line 32 assertion at file Test\.java line 32 function java::Test\.testShortToLong:\(\)V bytecode-index 13: SUCCESS
+\[java::Test\.testShortToLong:\(\)V.assertion\.2\] line 33 assertion at file Test\.java line 33 function java::Test\.testShortToLong:\(\)V bytecode-index 19: FAILURE
+^EXIT=10$
+^SIGNAL=0$