From 6abaf25b81ee4f711dc560dd13360a9c5a4988e5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 6 Apr 2019 20:10:45 +0100 Subject: [PATCH] remove java_method_typet::final/native This removes four methods from java_method_typet. They do not belong there, as neither 'native' nor 'final' are part of the type of the method (they are field modifiers). They are never read. --- .../java_bytecode_convert_method.cpp | 3 -- jbmc/src/java_bytecode/java_types.h | 20 ------------- .../convert_method.cpp | 29 ------------------- 3 files changed, 52 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index de630a71dac..1aa56917b12 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -326,7 +326,6 @@ 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); member_type.set_is_varargs(m.is_varargs); member_type.set_is_synthetic(m.is_synthetic); @@ -418,7 +417,6 @@ void java_bytecode_convert_methodt::convert( // to the symbol later. java_method_typet method_type = to_java_method_type(symbol_table.lookup_ref(method_identifier).type); - method_type.set_is_final(m.is_final); method_return_type = method_type.return_type(); java_method_typet::parameterst ¶meters = method_type.parameters(); @@ -2231,7 +2229,6 @@ void java_bytecode_convert_methodt::convert_invoke( id2string(symbol.base_name) + "()"; symbol.type = method_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( diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 4b5587aad4f..6eb11407862 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -136,26 +136,6 @@ 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); - } - - bool get_native() const - { - return get_bool(ID_is_native_method); - } - - void set_native(bool is_native) - { - set(ID_is_native_method, is_native); - } - bool get_is_varargs() const { return get_bool(ID_is_varargs_method); 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 213dfdcd927..2a0e62bffc8 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 @@ -89,10 +89,6 @@ SCENARIO( { 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()); - } THEN("The method should be marked as declared by its class") { REQUIRE( @@ -104,13 +100,6 @@ SCENARIO( { 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 not be marked as a native method.") - { - REQUIRE_FALSE(to_java_method_type(function_type).get_native()); - } THEN("The method should be marked as declared by its class") { REQUIRE( @@ -134,12 +123,6 @@ SCENARIO( { 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()); - } THEN("The method should be marked as declared by its class") { REQUIRE( @@ -151,12 +134,6 @@ SCENARIO( { 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()); - } THEN("The method should be marked as declared by its class") { REQUIRE( @@ -168,12 +145,6 @@ SCENARIO( { 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()); - } THEN("The method should be marked as declared by its class") { REQUIRE(