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.

Author: Daniel Kroening

Diff for: jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -340,7 +340,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);
 
   if(m.is_bridge)
@@ -431,7 +430,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 &parameters = method_type.parameters();
 
@@ -2212,7 +2210,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 for: jbmc/src/java_bytecode/java_types.h

@@ -364,26 +364,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 for: jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -86,10 +86,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(
@@ -101,13 +97,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(
@@ -131,12 +120,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(
@@ -148,12 +131,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(
@@ -165,12 +142,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(