Add test checking generic function parameter casts appear when expected

Author: smowton

jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+--function test.main2 --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+this \. test.callee2:\(Ltest;\)V\(\(struct test \*\)param\);
+--
+--
+test and callee2 have differing parameter types, so there should be a cast at the callsite.

jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+--function test.main --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+this \. test.callee:\(Ltest;\)V\(param\);
+--
+--
+test and callee have matching parameter types, so there should be no cast at the callsite.

jbmc/regression/jbmc/generic_function_parameter/ensure_runs.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+--function test.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::test.callee:\(Ltest;\)V\.assertion\.1\] line 12 assertion at file test\.java line 12 function java::test\.callee:\(Ltest;\)V bytecode-index 5: FAILURE$
+--
+^warning: ignoring

jbmc/regression/jbmc/generic_function_parameter/ensure_runs2.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+--function test.main2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::test.callee2:\(Ltest;\)V\.assertion\.1\] line 24 assertion at file test\.java line 24 function java::test\.callee2:\(Ltest;\)V bytecode-index 5: FAILURE$
+--
+^warning: ignoring

jbmc/regression/jbmc/generic_function_parameter/test.class

@@ -0,0 +1,28 @@
+
+public class test<T> {
+
+  public void main(test<String> param) {
+
+    callee(param);
+
+  }
+
+  public void callee(test<String> param) {
+
+    assert false;
+
+  }
+
+  public void main2(test<String> param) {
+
+    callee2((test<T>)param);
+
+  }
+
+  public void callee2(test<T> param) {
+
+    assert false;
+
+  }
+
+}