Merge pull request #1731 from diffblue/bugfix/all_resolved_calls

[TG-1931] Resolve calls to java.lang.Object functions to more specific ones

Author: Matthias Güdemann

regression/cbmc-java/virtual10/A.class

@@ -0,0 +1,6 @@
+CORE
+E.class
+--show-goto-functions
+IF.*"java::D"
+IF.*"java::O"
+IF.*"java::C"

regression/cbmc-java/virtual10/B.class

@@ -0,0 +1,35 @@
+interface A {
+  public int f();
+}
+interface B {
+  public int g();
+}
+
+class O {
+  public String toString() {
+    return "O";
+  }
+}
+
+class D extends O implements A, B {
+  public int f() {
+    return 0;
+  }
+  public int g() {
+    return 1;
+  }
+}
+
+class C extends D {
+  public String toString() {
+    return "C";
+  }
+}
+
+class E {
+  C c;
+  D d;
+  String f(Object o) {
+    return o.toString();
+  }
+}

regression/cbmc-java/virtual10/C.class

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

regression/cbmc-java/virtual10/D.class

@@ -3,9 +3,6 @@ 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
+IF.*"java::C".*THEN GOTO [12]
+IF.*"java::D".*THEN GOTO [12]
+IF.*"java::A".*THEN GOTO [12]