Add test for vtable abbreviation

Also amend virtual6 whose expected results are now
slightly different.

Author: smowton

regression/cbmc-java/virtual6/test.desc

@@ -5,4 +5,3 @@ A.class
 ^SIGNAL=0$
 IF "java::C".*THEN GOTO
 IF "java::B".*THEN GOTO
-IF "java::A".*THEN GOTO

regression/cbmc-java/virtual7/A.class

@@ -0,0 +1,12 @@
+CORE
+test.class
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+IF "java::E".*THEN GOTO [12]
+IF "java::B".*THEN GOTO [12]
+IF "java::D".*THEN GOTO [12]
+IF "java::C".*THEN GOTO [12]
+--
+IF "java::A".*THEN GOTO
+GOTO 4

regression/cbmc-java/virtual7/B.class

@@ -0,0 +1,25 @@
+public class test {
+  public static void main() {
+    A[] as = { new A(), new B(), new C(), new D(), new E() };
+    as[2].f();
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}