diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index d9229922ab7..668b2c1e02b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 4792231cdd7..2da36401905 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/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 <> diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class new file mode 100644 index 00000000000..85b3b507176 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java new file mode 100644 index 00000000000..58351bf9159 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java @@ -0,0 +1,6 @@ +public class ClassWithNativeMethod { + native boolean f(); + boolean f(int i) { + return false; + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index 8c0e45c18ef..db4ef399943 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -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( diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ca742f83b6f..cfbfe482ba0 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -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)