Fix virtual method resolution for Java Object parameters

jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java

@@ -0,0 +1,22 @@
+// Simpler test case demonstrating the virtual method resolution bug
+public class SimpleEquals {
+  public static void testDirect() {
+    // Direct call on String - this works
+    String s1 = "hello";
+    String s2 = "hello";
+    assert(s1.equals(s2));
+  }
+
+  public static void testThroughObject(Object o1, Object o2) {
+    // Call through Object parameter - this was failing before the fix
+    assert(o1.equals(o2));
+  }
+
+  public static void main(String[] args) {
+    testDirect();
+
+    String s1 = "world";
+    String s2 = "world";
+    testThroughObject(s1, s2);
+  }
+}

jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java

@@ -0,0 +1,13 @@
+public class equals_Pass {
+  private static boolean myEquals(Object a, Object b) {
+      return (a == b) || (a != null && a.equals(b));
+  }
+
+  public static void main(String[] args) {
+    String a = new String("abc");
+    String b = new String("abc");
+    assert((a == b) || (a != null && a.equals(b)));  // This passes
+    boolean result = myEquals(a, b);
+    assert(result);  // This fails
+  }
+}

jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc

@@ -0,0 +1,9 @@
+CORE
+SimpleEquals.class
+--function SimpleEquals.main
+^EXIT=0$
+^SIGNAL=0$
+^\[SimpleEquals.testDirect.assertion.1\] line 6 .*: SUCCESS$
+^\[SimpleEquals.testThroughObject.assertion.1\] line 11 .*: SUCCESS$
+--
+^warning: ignoring

jbmc/regression/jbmc/virtual_equals_object_param/test.desc

@@ -0,0 +1,9 @@
+CORE
+equals_Pass.class
+--function equals_Pass.main
+^EXIT=0$
+^SIGNAL=0$
+^\[equals_Pass.main.assertion.1\] line 9 .*: SUCCESS$
+^\[equals_Pass.main.assertion.2\] line 11 .*: SUCCESS$
+--
+^warning: ignoring

src/goto-programs/remove_virtual_functions.cpp

@@ -518,13 +518,12 @@ void get_virtual_calleest::get_child_functions_rec(
   for(const auto &child : findit->second.children)
   {
     // Skip if we have already visited this and we found a function call that
-    // did not resolve to non java.lang.Object.
+    // resolved to a non-Object implementation (i.e., we don't need to revisit).
     auto it = entry_map.find(child);
     if(
-      it != entry_map.end() &&
-      (!it->second.symbol_expr.has_value() ||
-       !it->second.symbol_expr->get_identifier().starts_with(
-         "java::java.lang.Object")))
+      it != entry_map.end() && it->second.symbol_expr.has_value() &&
+      !it->second.symbol_expr->get_identifier().starts_with(
+        "java::java.lang.Object"))
     {
       continue;
     }