Add test for casting of virtual function parameter types

jbmc/regression/jbmc/generic_virtual_function/Base.java

@@ -0,0 +1,33 @@
+
+public class Base<T> {
+
+  public T genericData;
+  public String nonGenericData;
+
+  public void main(boolean unknown1, boolean unknown2) {
+
+    Base b = unknown1 ? new Impl1<T>() : new Impl2<T>();
+    if(unknown2)
+      b.f(genericData);
+    else
+      b.g(nonGenericData);
+  }
+
+  public void f(T t) { }
+  public void g(String t) { }
+
+}
+
+class Impl1<T> extends Base<T> {
+
+  public void f(T t) { assert false; }
+  public void g(String t) { assert false; }
+
+}
+
+class Impl2<T> extends Base<T> {
+
+  public void f(T t) { assert false; }
+  public void g(String t) { assert false; }
+
+}

jbmc/regression/jbmc/generic_virtual_function/check_casts.desc

@@ -0,0 +1,14 @@
+CORE
+Base.class
+--function Base.main --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+\(struct Impl1 \*\)b \. Impl1\.f:\(Ljava/lang/Object;\)V\(\(struct java\.lang\.Object \*\)this->genericData\);
+\(struct Impl2 \*\)b \. Impl2\.f:\(Ljava/lang/Object;\)V\(\(struct java\.lang\.Object \*\)this->genericData\);
+\(struct Impl2 \*\)b \. Impl2\.g:\(Ljava/lang/String;\)V\(this->nonGenericData\);
+\(struct Impl1 \*\)b \. Impl1\.g:\(Ljava/lang/String;\)V\(this->nonGenericData\);
+--
+--
+Both the implementation classes use a different generic token (Impl1::T and Impl2::T) to refer
+to the generically-typed method f() and so a cast is needed. By contrast the concrete-typed
+virtual method g() does not need one.

jbmc/regression/jbmc/generic_virtual_function/ensure_runs.desc

@@ -0,0 +1,10 @@
+CORE
+Base.class
+--function Base.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::Impl1\.f:\(Ljava/lang/Object;\)V.assertion\.1\] line 23 assertion at file Base.java line 23 function java::Impl1\.f:\(Ljava/lang/Object;\)V bytecode-index 5: FAILURE
+\[java::Impl1\.g:\(Ljava/lang/String;\)V.assertion\.1\] line 24 assertion at file Base.java line 24 function java::Impl1\.g:\(Ljava/lang/String;\)V bytecode-index 5: FAILURE
+\[java::Impl2\.f:\(Ljava/lang/Object;\)V.assertion\.1\] line 30 assertion at file Base.java line 30 function java::Impl2\.f:\(Ljava/lang/Object;\)V bytecode-index 5: FAILURE
+\[java::Impl2\.g:\(Ljava/lang/String;\)V.assertion\.1\] line 31 assertion at file Base.java line 31 function java::Impl2\.g:\(Ljava/lang/String;\)V bytecode-index 5: FAILURE