Merge pull request #2888 from diffblue/feature/jbmc/mark_ACC_NATIVE_java_methods

Mark native methods `java_method_typet` with `ID_is_native_method`

Author: Matthias Güdemann

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -372,6 +372,7 @@ void java_bytecode_convert_method_lazy(
     member_type.set(ID_is_synchronized, true);
   if(m.is_static)
     member_type.set(ID_is_static, true);
+  member_type.set_native(m.is_native);
 
   if(m.is_bridge)
     member_type.set(ID_is_bridge_method, m.is_bridge);

jbmc/src/java_bytecode/java_types.h

@@ -288,6 +288,16 @@ class java_method_typet : public code_typet
   {
     set(ID_final, is_final);
   }
+
+  bool get_native() const
+  {
+    return get_bool(ID_is_native_method);
+  }
+
+  void set_native(bool is_native)
+  {
+    set(ID_is_native_method, is_native);
+  }
 };
 
 template <>

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class

@@ -0,0 +1,6 @@
+public class ClassWithNativeMethod {
+  native boolean f();
+  boolean f(int i) {
+    return false;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
- Module: Unit tests for converting constructors and static initializers
+ Module: Unit tests for converting methods.
 
  Author: Diffblue Limited.
 
@@ -56,6 +56,45 @@ SCENARIO(
       }
     }
   }
+  GIVEN("A class with a native method")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassWithNativeMethod", "./java_bytecode/java_bytecode_convert_method");
+
+    const std::string method_name = "java::ClassWithNativeMethod.f";
+
+    WHEN("When parsing the native method")
+    {
+      const symbolt function_symbol =
+        symbol_table.lookup_ref(method_name + ":()Z");
+
+      const java_method_typet &function_type =
+        require_type::require_java_method(function_symbol.type);
+      THEN("The method symbol should be of java_method_typet")
+      {
+        REQUIRE(function_type.get_bool(ID_C_java_method_type));
+      }
+      THEN("And the method should be marked as a native method")
+      {
+        REQUIRE(to_java_method_type(function_type).get_native());
+      }
+    }
+    WHEN("When parsing a non-native method")
+    {
+      THEN("THe method should not be marked as a native method")
+      {
+        const symbolt function_symbol =
+          symbol_table.lookup_ref(method_name + ":(I)Z");
+
+        const java_method_typet &function_type =
+          require_type::require_java_method(function_symbol.type);
+        THEN("The method should be marked as a native method")
+        {
+          REQUIRE_FALSE(to_java_method_type(function_type).get_native());
+        }
+      }
+    }
+  }
 }
 
 SCENARIO(

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -387,6 +387,7 @@ IREP_ID_ONE(is_enum_constant)
 IREP_ID_ONE(is_inline)
 IREP_ID_ONE(is_extern)
 IREP_ID_ONE(is_synchronized)
+IREP_ID_ONE(is_native_method)
 IREP_ID_ONE(is_global)
 IREP_ID_ONE(is_thread_local)
 IREP_ID_ONE(is_parameter)