Merge pull request #2895 from allredj/for-final-mocking-opaque

Set opaque methods as final

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2197,6 +2197,7 @@ void java_bytecode_convert_methodt::convert_invoke(
   // - The translated method could be an inherited protected method, hence
   //   accessible from the original caller, but not from the generated test.
   //   Therefore we must assume that the method is not accessible.
+  // We set opaque methods as final to avoid assuming they can be overridden.
   irep_idt id = arg0.get(ID_identifier);
   if(
     symbol_table.symbols.find(id) == symbol_table.symbols.end() &&
@@ -2210,6 +2211,7 @@ void java_bytecode_convert_methodt::convert_invoke(
                          id2string(symbol.base_name) + "()";
     symbol.type = arg0.type();
     symbol.type.set(ID_access, ID_private);
+    to_java_method_type(symbol.type).set_is_final(true);
     symbol.value.make_nil();
     symbol.mode = ID_java;
     assign_parameter_names(

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithFinalMethod.class

@@ -5,4 +5,7 @@ public final int finalFunc() {
   public int nonFinalFunc() {
     return 0;
   }
+  public int opaqueFunc() {
+    return OpaqueClass.staticFunc();
+  }
 }

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithFinalMethod.java

@@ -0,0 +1,6 @@
+// .class file must be deleted
+public class OpaqueClass {
+  public static int staticFunc() {
+    return 0;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/OpaqueClass.java

@@ -89,5 +89,16 @@ SCENARIO(
         REQUIRE(!function_type.get_is_final());
       }
     }
+    WHEN("When parsing an opaque method")
+    {
+      const symbolt function_symbol =
+        symbol_table.lookup_ref("java::OpaqueClass.staticFunc:()I");
+      const java_method_typet &function_type =
+        require_type::require_java_method(function_symbol.type);
+      THEN("The method should be marked as final")
+      {
+        REQUIRE(function_type.get_is_final());
+      }
+    }
   }
 }