Add support for recording and propagating class access flags

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -86,7 +86,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
     return;
   }
 
-  class_typet class_type;
+  java_class_typet class_type;
 
   class_type.set_tag(c.name);
   class_type.set(ID_base_name, c.name);
@@ -98,6 +98,15 @@ void java_bytecode_convert_classt::convert(const classt &c)
     class_type.set(ID_enumeration, true);
   }
 
+  if(c.is_public)
+    class_type.set_access(ID_public);
+  else if(c.is_protected)
+    class_type.set_access(ID_protected);
+  else if(c.is_private)
+    class_type.set_access(ID_private);
+  else
+    class_type.set_access(ID_default);
+
   if(!c.extends.empty())
   {
     symbol_typet base("java::"+id2string(c.extends));

src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -26,6 +26,9 @@ void java_bytecode_parse_treet::classt::swap(
   std::swap(other.is_enum, is_enum);
   std::swap(other.enum_elements, enum_elements);
   std::swap(other.is_abstract, is_abstract);
+  std::swap(other.is_public, is_public);
+  std::swap(other.is_protected, is_protected);
+  std::swap(other.is_private, is_private);
   other.implements.swap(implements);
   other.fields.swap(fields);
   other.methods.swap(methods);

src/java_bytecode/java_bytecode_parse_tree.h

@@ -169,6 +169,7 @@ class java_bytecode_parse_treet
     irep_idt name, extends;
     bool is_abstract=false;
     bool is_enum=false;
+    bool is_public=false, is_protected=false, is_private=false;
     size_t enum_elements=0;
 
     typedef std::list<irep_idt> implementst;

src/java_bytecode/java_bytecode_parser.cpp

@@ -279,6 +279,9 @@ void java_bytecode_parsert::rClassFile()
 
   parsed_class.is_abstract=(access_flags&ACC_ABSTRACT)!=0;
   parsed_class.is_enum=(access_flags&ACC_ENUM)!=0;
+  parsed_class.is_public=(access_flags&ACC_PUBLIC)!=0;
+  parsed_class.is_protected=(access_flags&ACC_PROTECTED)!=0;
+  parsed_class.is_private=(access_flags&ACC_PRIVATE)!=0;
   parsed_class.name=
     constant(this_class).type().get(ID_C_base_name);
 

src/java_bytecode/java_types.h

@@ -13,6 +13,32 @@ Author: Daniel Kroening, [email protected]
 #include <util/type.h>
 #include <util/std_types.h>
 
+class java_class_typet:public class_typet
+{
+ public:
+  const irep_idt &get_access() const
+  {
+    return get(ID_access);
+  }
+
+  void set_access(const irep_idt &access)
+  {
+    return set(ID_access, access);
+  }
+};
+
+inline const java_class_typet &to_java_class_type(const typet &type)
+{
+  assert(type.id()==ID_struct);
+  return static_cast<const java_class_typet &>(type);
+}
+
+inline java_class_typet &to_java_class_type(typet &type)
+{
+  assert(type.id()==ID_struct);
+  return static_cast<java_class_typet &>(type);
+}
+
 typet java_int_type();
 typet java_long_type();
 typet java_short_type();