Introduce getters/setters for java class properties

The IDs are used already; this commit merely adds a wrapper.

The consistency of using the "is_" prefix should be considered as a separate
PR.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -311,10 +311,10 @@ void java_bytecode_convert_classt::convert(
 
   class_type.set_tag(c.name);
   class_type.set_inner_name(c.inner_name);
-  class_type.set(ID_abstract, c.is_abstract);
-  class_type.set(ID_is_annotation, c.is_annotation);
-  class_type.set(ID_interface, c.is_interface);
-  class_type.set(ID_synthetic, c.is_synthetic);
+  class_type.set_abstract(c.is_abstract);
+  class_type.set_is_annotation(c.is_annotation);
+  class_type.set_interface(c.is_interface);
+  class_type.set_synthetic(c.is_synthetic);
   class_type.set_final(c.is_final);
   class_type.set_is_inner_class(c.is_inner_class);
   class_type.set_is_static_class(c.is_static_class);

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -188,6 +188,8 @@ static void java_static_lifetime_init(
         // For arguments we can't parse yet:
         side_effect_expr_nondett nondet_bool(java_boolean_type(), sym.location);
 
+        const auto &java_class_type = to_java_class_type(class_symbol.type);
+
         // Argument order is: name, isAnnotation, isArray, isInterface,
         // isSynthetic, isLocalClass, isMemberClass, isEnum
 
@@ -198,19 +200,19 @@ static void java_static_lifetime_init(
            // name:
            address_of_exprt(class_name_literal),
            // isAnnotation:
-           constant_bool(class_symbol.type.get_bool(ID_is_annotation)),
+           constant_bool(java_class_type.get_is_annotation()),
            // isArray:
            constant_bool(class_is_array),
            // isInterface:
-           constant_bool(class_symbol.type.get_bool(ID_interface)),
+           constant_bool(java_class_type.get_interface()),
            // isSynthetic:
-           constant_bool(class_symbol.type.get_bool(ID_synthetic)),
+           constant_bool(java_class_type.get_synthetic()),
            // isLocalClass:
            nondet_bool,
            // isMemberClass:
            nondet_bool,
            // isEnum:
-           constant_bool(class_symbol.type.get_bool(ID_enumeration))});
+           constant_bool(java_class_type.get_is_enumeration())});
 
         // First initialize the object as prior to a constructor:
         namespacet ns(symbol_table);

jbmc/src/java_bytecode/java_types.h

@@ -402,6 +402,54 @@ class java_class_typet:public class_typet
     set(ID_enumeration, is_enumeration);
   }
 
+  /// is class abstract?
+  bool get_abstract() const
+  {
+    return get_bool(ID_abstract);
+  }
+
+  /// marks class abstract
+  void set_abstract(bool abstract)
+  {
+    set(ID_abstract, abstract);
+  }
+
+  /// is class synthetic?
+  bool get_synthetic() const
+  {
+    return get_bool(ID_synthetic);
+  }
+
+  /// marks class synthetic
+  void set_synthetic(bool synthetic)
+  {
+    set(ID_synthetic, synthetic);
+  }
+
+  /// is class an annotation?
+  bool get_is_annotation() const
+  {
+    return get_bool(ID_is_annotation);
+  }
+
+  /// marks class an annotation
+  void set_is_annotation(bool is_annotation)
+  {
+    set(ID_is_annotation, is_annotation);
+  }
+
+  /// is class an interface?
+  bool get_interface() const
+  {
+    return get_bool(ID_interface);
+  }
+
+  /// marks class an interface
+  void set_interface(bool interface)
+  {
+    set(ID_interface, interface);
+  }
+
   // it may be better to introduce a class like
   // class java_lambda_method_handlet : private irept
   // {