Merge pull request #4201 from smowton/smowton/cleanup/cast-base-type-test

Add test for casting after a clean or soft cast

Author: smowton

jbmc/regression/jbmc/generic_base_type/Base.class

@@ -0,0 +1,21 @@
+
+public class Base<T> { }
+
+class Test<T> extends Base<T> {
+
+  public void main(boolean unknown) {
+
+    if(unknown)
+      callee(getSpecialisedTest());
+    else
+      callee2(getUnspecialisedTest());
+
+  }
+
+  public Test<String> getSpecialisedTest() { return new Test<String>(); }
+  public Test<T> getUnspecialisedTest() { return new Test<T>(); }
+
+  public void callee(Base<String> b) { assert false; }
+  public void callee2(Base<T> b) { assert false; }
+
+}

jbmc/regression/jbmc/generic_base_type/Base.java

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.main --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+this \. Test\.callee:\(LBase;\)V\(\(struct Base \*\)&return_tmp0->@Base\);
+this \. Test\.callee2:\(LBase;\)V\(&return_tmp1->@Base\);
+--
+callee has a qualified Base type, and so requires a cast.
+callee2 has the unqualified type that Test<T> naturally inherits, so no cast is required.

jbmc/regression/jbmc/generic_base_type/Test.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::Test\.callee:\(LBase;\)V\.assertion\.1\] line 18 assertion at file Base\.java line 18 function java::Test\.callee:\(LBase;\)V bytecode-index 5: FAILURE
+\[java::Test\.callee2:\(LBase;\)V\.assertion\.1\] line 19 assertion at file Base\.java line 19 function java::Test\.callee2:\(LBase;\)V bytecode-index 5: FAILURE
+--
+^warning: ignoring