Merge pull request #404 from smowton/shorten_virtual_dispatch_tables

Shorten virtual dispatch tables

Author: peterschrammel

regression/cbmc-java/NullPointer2/test.desc

@@ -3,7 +3,7 @@ NullPointer2.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V$
+^  file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

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 {
+}