move is_final to java component type

'final' is a field modifier for Java, and has no meaning in C or C++.  It
should thus move to java_class_typet::componentt.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -740,10 +740,10 @@ void java_bytecode_convert_classt::convert(
   }
   else
   {
-    class_typet &class_type=to_class_type(class_symbol.type);
+    auto &class_type = to_java_class_type(class_symbol.type);
 
     class_type.components().emplace_back();
-    class_typet::componentt &component=class_type.components().back();
+    auto &component = class_type.components().back();
 
     component.set_name(f.name);
     component.set_base_name(f.name);

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -332,7 +332,7 @@ static void infer_opaque_type_fields(
             symbolt &writable_class_symbol =
               symbol_table.get_writeable_ref(class_symbol_id);
             auto &components =
-              to_struct_type(writable_class_symbol.type).components();
+              to_java_class_type(writable_class_symbol.type).components();
             components.emplace_back(component_name, fieldref.type());
             components.back().set_base_name(component_name);
             components.back().set_pretty_name(component_name);

jbmc/src/java_bytecode/java_types.h

@@ -112,6 +112,18 @@ class java_class_typet:public class_typet
     {
     }
 
+    /// is a method or field 'final'?
+    bool get_is_final() const
+    {
+      return get_bool(ID_final);
+    }
+
+    /// is a method or field 'final'?
+    void set_is_final(const bool is_final)
+    {
+      set(ID_final, is_final);
+    }
+
     /// is a method 'native'?
     bool get_is_native() const
     {
@@ -137,6 +149,12 @@ class java_class_typet:public class_typet
     return (componentst &)(add(ID_components).get_sub());
   }
 
+  const componentt &get_component(const irep_idt &component_name) const
+  {
+    return static_cast<const componentt &>(
+      class_typet::get_component(component_name));
+  }
+
   const irep_idt &get_access() const
   {
     return get(ID_access);

jbmc/unit/java-testing-utils/require_type.cpp

@@ -30,11 +30,30 @@ pointer_typet require_type::require_pointer(
   return pointer;
 }
 
+/// Checks that a class has a component with a specific name
+/// \param java_class_type: The class that should have the component
+/// \param component_name: The name of the component
+/// \return The component with the specified name
+java_class_typet::componentt require_type::require_component(
+  const java_class_typet &java_class_type,
+  const irep_idt &component_name)
+{
+  const auto &component = std::find_if(
+    java_class_type.components().begin(),
+    java_class_type.components().end(),
+    [&component_name](const java_class_typet::componentt &component) {
+      return component.get_name() == component_name;
+    });
+
+  REQUIRE(component != java_class_type.components().end());
+  return *component;
+}
+
 /// Checks a struct like type has a component with a specific name
 /// \param struct_type: The structure that should have the component
 /// \param component_name: The name of the component
 /// \return The component with the specified name
-struct_union_typet::componentt require_type::require_component(
+struct_typet::componentt require_type::require_component(
   const struct_typet &struct_type,
   const irep_idt &component_name)
 {

jbmc/unit/java-testing-utils/require_type.h

@@ -32,6 +32,10 @@ const pointer_typet require_pointer_to_tag(
   const typet &type,
   const irep_idt &identifier = irep_idt());
 
+java_class_typet::componentt require_component(
+  const java_class_typet &java_class_type,
+  const irep_idt &component_name);
+
 struct_typet::componentt require_component(
   const struct_typet &struct_type,
   const irep_idt &component_name);

jbmc/unit/java_bytecode/java_bytecode_language/language.cpp

@@ -36,9 +36,9 @@ SCENARIO(
       {
         const symbolt &opaque_class_symbol =
           symbol_table.lookup_ref(opaque_class_prefix);
-        const struct_typet &opaque_class_struct =
-          to_struct_type(opaque_class_symbol.type);
-        const struct_union_typet::componentt &field =
+        const auto &opaque_class_struct =
+          to_java_class_type(opaque_class_symbol.type);
+        const auto &field =
           require_type::require_component(opaque_class_struct, "field2");
         REQUIRE(field.get_is_final());
       }

src/util/std_types.h

@@ -123,16 +123,6 @@ class struct_union_typet:public typet
     {
       return set(ID_C_is_padding, is_padding);
     }
-
-    bool get_is_final() const
-    {
-      return get_bool(ID_final);
-    }
-
-    void set_is_final(const bool is_final)
-    {
-      set(ID_final, is_final);
-    }
   };
 
   typedef std::vector<componentt> componentst;