Merge pull request #2831 from allredj/for-final-mocking

Retrieve final qualifier from bytecode methods [TG-2893]

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -447,6 +447,7 @@ void java_bytecode_convert_methodt::convert(
   // (function) type of the symbol
   java_method_typet method_type = to_java_method_type(method_symbol.type);
   method_type.set(ID_C_class, class_symbol.name);
+  method_type.set_is_final(m.is_final);
   method_return_type = method_type.return_type();
   java_method_typet::parameterst &parameters = method_type.parameters();
 

jbmc/src/java_bytecode/java_types.h

@@ -278,6 +278,16 @@ class java_method_typet : public code_typet
   {
     add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
   }
+
+  bool get_is_final() const
+  {
+    return get_bool(ID_final);
+  }
+
+  void set_is_final(bool is_final)
+  {
+    set(ID_final, is_final);
+  }
 };
 
 template <>

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithFinalMethod.class

@@ -0,0 +1,8 @@
+public class ClassWithFinalMethod {
+  public final int finalFunc() {
+    return 0;
+  }
+  public int nonFinalFunc() {
+    return 0;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithFinalMethod.java

@@ -57,3 +57,37 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "java_bytecode_convert_final_method",
+  "[core][java_bytecode][java_bytecode_convert_method]")
+{
+  GIVEN("A class with final and non-final methods")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassWithFinalMethod", "./java_bytecode/java_bytecode_convert_method");
+
+    WHEN("When parsing a final method")
+    {
+      const symbolt function_symbol =
+        symbol_table.lookup_ref("java::ClassWithFinalMethod.finalFunc:()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());
+      }
+    }
+    WHEN("When parsing a non-final method")
+    {
+      const symbolt function_symbol =
+        symbol_table.lookup_ref("java::ClassWithFinalMethod.nonFinalFunc:()I");
+      const java_method_typet &function_type =
+        require_type::require_java_method(function_symbol.type);
+      THEN("The method should not be marked as final")
+      {
+        REQUIRE(!function_type.get_is_final());
+      }
+    }
+  }
+}