Merge pull request diffblue#2526 from jeannielynnmoulton/jeannie/AnonymousInnerClasses

Matthias Güdemann · web-flow · commit 8187bdd1652f · 2018-07-06T16:43:24.000+02:00
Captures anonymous inner class information
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -278,6 +278,7 @@ void java_bytecode_convert_classt::convert(
   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);
+  class_type.set_is_anonymous_class(c.is_anonymous_class);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -219,6 +219,7 @@ class java_bytecode_parse_treet
     bool is_annotation = false;
     bool is_inner_class = false;
     bool is_static_class = false;
+    bool is_anonymous_class = false;
     bool attribute_bootstrapmethods_read = false;
     size_t enum_elements=0;
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1613,7 +1613,7 @@ void java_bytecode_parsert::rinner_classes_attribute(
   {
     u2 inner_class_info_index = read_u2();
     u2 outer_class_info_index = read_u2();
-    UNUSED u2 inner_name_index = read_u2();
+    u2 inner_name_index = read_u2();
     u2 inner_class_access_flags = read_u2();
 
     std::string inner_class_info_name =
@@ -1634,6 +1634,9 @@ void java_bytecode_parsert::rinner_classes_attribute(
     if(!is_inner_class)
       continue;
     parsed_class.is_static_class = is_static;
+    // This is a marker that a class is anonymous.
+    if(inner_name_index == 0)
+      parsed_class.is_anonymous_class = true;
     // Note that if outer_class_info_index == 0, the inner class is an anonymous
     // or local class, and is treated as private.
     if(outer_class_info_index == 0)
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
@@ -131,6 +131,15 @@ class java_class_typet:public class_typet
     return set(ID_is_static, is_static_class);
   }
 
+  const bool get_is_anonymous_class() const
+  {
+    return get_bool(ID_is_anonymous);
+  }
+
+  void set_is_anonymous_class(const bool &is_anonymous_class)
+  {
+    return set(ID_is_anonymous, is_anonymous_class);
+  }
 
   bool get_final()
   {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
@@ -28,6 +28,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_public);
       }
@@ -40,6 +41,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_default);
       }
@@ -52,6 +54,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_protected);
       }
@@ -64,6 +67,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
@@ -81,6 +85,7 @@ SCENARIO(
           "java::InnerClassesDefault$PublicInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_public);
       }
@@ -93,6 +98,7 @@ SCENARIO(
           "java::InnerClassesDefault$DefaultInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_default);
       }
@@ -105,6 +111,7 @@ SCENARIO(
           "java::InnerClassesDefault$ProtectedInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_protected);
       }
@@ -117,6 +124,7 @@ SCENARIO(
           "java::InnerClassesDefault$PrivateInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
@@ -140,6 +148,7 @@ SCENARIO(
           "PublicDoublyNestedInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_public);
       }
@@ -155,6 +164,7 @@ SCENARIO(
           "DefaultDoublyNestedInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_default);
       }
@@ -170,6 +180,7 @@ SCENARIO(
           "ProtectedDoublyNestedInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_protected);
       }
@@ -185,6 +196,7 @@ SCENARIO(
           "PrivateDoublyNestedInnerClass");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
@@ -198,51 +210,55 @@ SCENARIO(
       "ContainsAnonymousClass", "./java_bytecode/java_bytecode_parser");
     WHEN("Parsing the InnerClasses attribute for a public anonymous class")
     {
-      THEN("The class should be marked as public")
+      THEN("The class should be marked as private and anonymous")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$1");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
     WHEN(
       "Parsing the InnerClasses attribute for a package-private anonymous "
       "class")
     {
-      THEN("The class should be marked as default")
+      THEN("The class should be marked as private and anonymous")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$2");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
     WHEN("Parsing the InnerClasses attribute for a protected anonymous class")
     {
-      THEN("The class should be marked as protected")
+      THEN("The class should be marked as private and anonymous")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$3");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
     WHEN("Parsing the InnerClasses attribute for a private anonymous class")
     {
-      THEN("The class should be marked as private")
+      THEN("The class should be marked as private and anonymous")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$4");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
@@ -263,6 +279,7 @@ SCENARIO(
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
       }
     }
   }
@@ -281,6 +298,7 @@ SCENARIO(
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_static_class());
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
       }
     }
     WHEN("Parsing the InnerClasses attribute for a non-static inner class ")
@@ -293,32 +311,35 @@ SCENARIO(
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
       }
     }
   }
   GIVEN("Some class with a static anonymous class")
   {
     WHEN("Parsing the InnerClasses attribute for a static anonymous class ")
     {
-      THEN("The class should be marked as static")
+      THEN("The class should be marked as static and anonymous")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::StaticInnerClass$1");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_static_class());
       }
     }
     WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ")
     {
-      THEN("The class should not be marked as static")
+      THEN("The class should be marked as anonymous and not static")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::StaticInnerClass$2");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
       }
     }
@@ -337,6 +358,7 @@ SCENARIO(
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
       }
     }
     WHEN(
@@ -351,6 +373,7 @@ SCENARIO(
           to_java_class_type(class_symbol.type);
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
       }
     }
   }
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -676,6 +676,7 @@ IREP_ID_TWO(C_must_not_throw, #must_not_throw)
 IREP_ID_ONE(always_inline)
 IREP_ID_ONE(is_always_inline)
 IREP_ID_ONE(is_inner_class)
+IREP_ID_ONE(is_anonymous)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.h in their source tree and

Original file line number	Diff line number	Diff line change
`@@ -278,6 +278,7 @@ void java_bytecode_convert_classt::convert(`
`278`	`278`	`class_type.set_final(c.is_final);`
`279`	`279`	`class_type.set_is_inner_class(c.is_inner_class);`
`280`	`280`	`class_type.set_is_static_class(c.is_static_class);`
	`281`	`+ class_type.set_is_anonymous_class(c.is_anonymous_class);`
`281`	`282`	`if(c.is_enum)`
`282`	`283`	`{`
`283`	`284`	`if(max_array_length != 0 && c.enum_elements > max_array_length)`
Original file line number	Diff line number	Diff line change
`@@ -131,6 +131,15 @@ class java_class_typet:public class_typet`
`131`	`131`	`return set(ID_is_static, is_static_class);`
`132`	`132`	`}`
`133`	`133`
	`134`	`+ const bool get_is_anonymous_class() const`
	`135`	`+ {`
	`136`	`+ return get_bool(ID_is_anonymous);`
	`137`	`+ }`
	`138`	`+`
	`139`	`+ void set_is_anonymous_class(const bool &is_anonymous_class)`
	`140`	`+ {`
	`141`	`+ return set(ID_is_anonymous, is_anonymous_class);`
	`142`	`+ }`
`134`	`143`
`135`	`144`	`bool get_final()`
`136`	`145`	`{`
Original file line number	Diff line number	Diff line change
`@@ -28,6 +28,7 @@ SCENARIO(`
`28`	`28`	`new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass");`
`29`	`29`	`const java_class_typet java_class =`
`30`	`30`	`to_java_class_type(class_symbol.type);`
	`31`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`31`	`32`	`REQUIRE(java_class.get_is_inner_class());`
`32`	`33`	`REQUIRE(java_class.get_access() == ID_public);`
`33`	`34`	`}`
`@@ -40,6 +41,7 @@ SCENARIO(`
`40`	`41`	`new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass");`
`41`	`42`	`const java_class_typet java_class =`
`42`	`43`	`to_java_class_type(class_symbol.type);`
	`44`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`43`	`45`	`REQUIRE(java_class.get_is_inner_class());`
`44`	`46`	`REQUIRE(java_class.get_access() == ID_default);`
`45`	`47`	`}`
`@@ -52,6 +54,7 @@ SCENARIO(`
`52`	`54`	`new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass");`
`53`	`55`	`const java_class_typet java_class =`
`54`	`56`	`to_java_class_type(class_symbol.type);`
	`57`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`55`	`58`	`REQUIRE(java_class.get_is_inner_class());`
`56`	`59`	`REQUIRE(java_class.get_access() == ID_protected);`
`57`	`60`	`}`
`@@ -64,6 +67,7 @@ SCENARIO(`
`64`	`67`	`new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass");`
`65`	`68`	`const java_class_typet java_class =`
`66`	`69`	`to_java_class_type(class_symbol.type);`
	`70`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`67`	`71`	`REQUIRE(java_class.get_is_inner_class());`
`68`	`72`	`REQUIRE(java_class.get_access() == ID_private);`
`69`	`73`	`}`
`@@ -81,6 +85,7 @@ SCENARIO(`
`81`	`85`	`"java::InnerClassesDefault$PublicInnerClass");`
`82`	`86`	`const java_class_typet java_class =`
`83`	`87`	`to_java_class_type(class_symbol.type);`
	`88`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`84`	`89`	`REQUIRE(java_class.get_is_inner_class());`
`85`	`90`	`REQUIRE(java_class.get_access() == ID_public);`
`86`	`91`	`}`
`@@ -93,6 +98,7 @@ SCENARIO(`
`93`	`98`	`"java::InnerClassesDefault$DefaultInnerClass");`
`94`	`99`	`const java_class_typet java_class =`
`95`	`100`	`to_java_class_type(class_symbol.type);`
	`101`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`96`	`102`	`REQUIRE(java_class.get_is_inner_class());`
`97`	`103`	`REQUIRE(java_class.get_access() == ID_default);`
`98`	`104`	`}`
`@@ -105,6 +111,7 @@ SCENARIO(`
`105`	`111`	`"java::InnerClassesDefault$ProtectedInnerClass");`
`106`	`112`	`const java_class_typet java_class =`
`107`	`113`	`to_java_class_type(class_symbol.type);`
	`114`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`108`	`115`	`REQUIRE(java_class.get_is_inner_class());`
`109`	`116`	`REQUIRE(java_class.get_access() == ID_protected);`
`110`	`117`	`}`
`@@ -117,6 +124,7 @@ SCENARIO(`
`117`	`124`	`"java::InnerClassesDefault$PrivateInnerClass");`
`118`	`125`	`const java_class_typet java_class =`
`119`	`126`	`to_java_class_type(class_symbol.type);`
	`127`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`120`	`128`	`REQUIRE(java_class.get_is_inner_class());`
`121`	`129`	`REQUIRE(java_class.get_access() == ID_private);`
`122`	`130`	`}`
`@@ -140,6 +148,7 @@ SCENARIO(`
`140`	`148`	`"PublicDoublyNestedInnerClass");`
`141`	`149`	`const java_class_typet java_class =`
`142`	`150`	`to_java_class_type(class_symbol.type);`
	`151`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`143`	`152`	`REQUIRE(java_class.get_is_inner_class());`
`144`	`153`	`REQUIRE(java_class.get_access() == ID_public);`
`145`	`154`	`}`
`@@ -155,6 +164,7 @@ SCENARIO(`
`155`	`164`	`"DefaultDoublyNestedInnerClass");`
`156`	`165`	`const java_class_typet java_class =`
`157`	`166`	`to_java_class_type(class_symbol.type);`
	`167`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`158`	`168`	`REQUIRE(java_class.get_is_inner_class());`
`159`	`169`	`REQUIRE(java_class.get_access() == ID_default);`
`160`	`170`	`}`
`@@ -170,6 +180,7 @@ SCENARIO(`
`170`	`180`	`"ProtectedDoublyNestedInnerClass");`
`171`	`181`	`const java_class_typet java_class =`
`172`	`182`	`to_java_class_type(class_symbol.type);`
	`183`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`173`	`184`	`REQUIRE(java_class.get_is_inner_class());`
`174`	`185`	`REQUIRE(java_class.get_access() == ID_protected);`
`175`	`186`	`}`
`@@ -185,6 +196,7 @@ SCENARIO(`
`185`	`196`	`"PrivateDoublyNestedInnerClass");`
`186`	`197`	`const java_class_typet java_class =`
`187`	`198`	`to_java_class_type(class_symbol.type);`
	`199`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`188`	`200`	`REQUIRE(java_class.get_is_inner_class());`
`189`	`201`	`REQUIRE(java_class.get_access() == ID_private);`
`190`	`202`	`}`
`@@ -198,51 +210,55 @@ SCENARIO(`
`198`	`210`	`"ContainsAnonymousClass", "./java_bytecode/java_bytecode_parser");`
`199`	`211`	`WHEN("Parsing the InnerClasses attribute for a public anonymous class")`
`200`	`212`	`{`
`201`		`- THEN("The class should be marked as public")`
	`213`	`+ THEN("The class should be marked as private and anonymous")`
`202`	`214`	`{`
`203`	`215`	`const symbolt &class_symbol =`
`204`	`216`	`new_symbol_table.lookup_ref("java::ContainsAnonymousClass$1");`
`205`	`217`	`const java_class_typet java_class =`
`206`	`218`	`to_java_class_type(class_symbol.type);`
`207`	`219`	`REQUIRE(java_class.get_is_inner_class());`
	`220`	`+ REQUIRE(java_class.get_is_anonymous_class());`
`208`	`221`	`REQUIRE(java_class.get_access() == ID_private);`
`209`	`222`	`}`
`210`	`223`	`}`
`211`	`224`	`WHEN(`
`212`	`225`	`"Parsing the InnerClasses attribute for a package-private anonymous "`
`213`	`226`	`"class")`
`214`	`227`	`{`
`215`		`- THEN("The class should be marked as default")`
	`228`	`+ THEN("The class should be marked as private and anonymous")`
`216`	`229`	`{`
`217`	`230`	`const symbolt &class_symbol =`
`218`	`231`	`new_symbol_table.lookup_ref("java::ContainsAnonymousClass$2");`
`219`	`232`	`const java_class_typet java_class =`
`220`	`233`	`to_java_class_type(class_symbol.type);`
`221`	`234`	`REQUIRE(java_class.get_is_inner_class());`
	`235`	`+ REQUIRE(java_class.get_is_anonymous_class());`
`222`	`236`	`REQUIRE(java_class.get_access() == ID_private);`
`223`	`237`	`}`
`224`	`238`	`}`
`225`	`239`	`WHEN("Parsing the InnerClasses attribute for a protected anonymous class")`
`226`	`240`	`{`
`227`		`- THEN("The class should be marked as protected")`
	`241`	`+ THEN("The class should be marked as private and anonymous")`
`228`	`242`	`{`
`229`	`243`	`const symbolt &class_symbol =`
`230`	`244`	`new_symbol_table.lookup_ref("java::ContainsAnonymousClass$3");`
`231`	`245`	`const java_class_typet java_class =`
`232`	`246`	`to_java_class_type(class_symbol.type);`
`233`	`247`	`REQUIRE(java_class.get_is_inner_class());`
	`248`	`+ REQUIRE(java_class.get_is_anonymous_class());`
`234`	`249`	`REQUIRE(java_class.get_access() == ID_private);`
`235`	`250`	`}`
`236`	`251`	`}`
`237`	`252`	`WHEN("Parsing the InnerClasses attribute for a private anonymous class")`
`238`	`253`	`{`
`239`		`- THEN("The class should be marked as private")`
	`254`	`+ THEN("The class should be marked as private and anonymous")`
`240`	`255`	`{`
`241`	`256`	`const symbolt &class_symbol =`
`242`	`257`	`new_symbol_table.lookup_ref("java::ContainsAnonymousClass$4");`
`243`	`258`	`const java_class_typet java_class =`
`244`	`259`	`to_java_class_type(class_symbol.type);`
`245`	`260`	`REQUIRE(java_class.get_is_inner_class());`
	`261`	`+ REQUIRE(java_class.get_is_anonymous_class());`
`246`	`262`	`REQUIRE(java_class.get_access() == ID_private);`
`247`	`263`	`}`
`248`	`264`	`}`
`@@ -263,6 +279,7 @@ SCENARIO(`
`263`	`279`	`to_java_class_type(class_symbol.type);`
`264`	`280`	`REQUIRE(java_class.get_is_inner_class());`
`265`	`281`	`REQUIRE(java_class.get_access() == ID_private);`
	`282`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`266`	`283`	`}`
`267`	`284`	`}`
`268`	`285`	`}`
`@@ -281,6 +298,7 @@ SCENARIO(`
`281`	`298`	`to_java_class_type(class_symbol.type);`
`282`	`299`	`REQUIRE(java_class.get_is_inner_class());`
`283`	`300`	`REQUIRE(java_class.get_is_static_class());`
	`301`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`284`	`302`	`}`
`285`	`303`	`}`
`286`	`304`	`WHEN("Parsing the InnerClasses attribute for a non-static inner class ")`
`@@ -293,32 +311,35 @@ SCENARIO(`
`293`	`311`	`to_java_class_type(class_symbol.type);`
`294`	`312`	`REQUIRE(java_class.get_is_inner_class());`
`295`	`313`	`REQUIRE_FALSE(java_class.get_is_static_class());`
	`314`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`296`	`315`	`}`
`297`	`316`	`}`
`298`	`317`	`}`
`299`	`318`	`GIVEN("Some class with a static anonymous class")`
`300`	`319`	`{`
`301`	`320`	`WHEN("Parsing the InnerClasses attribute for a static anonymous class ")`
`302`	`321`	`{`
`303`		`- THEN("The class should be marked as static")`
	`322`	`+ THEN("The class should be marked as static and anonymous")`
`304`	`323`	`{`
`305`	`324`	`const symbolt &class_symbol =`
`306`	`325`	`new_symbol_table.lookup_ref("java::StaticInnerClass$1");`
`307`	`326`	`const java_class_typet java_class =`
`308`	`327`	`to_java_class_type(class_symbol.type);`
`309`	`328`	`REQUIRE(java_class.get_is_inner_class());`
	`329`	`+ REQUIRE(java_class.get_is_anonymous_class());`
`310`	`330`	`REQUIRE(java_class.get_is_static_class());`
`311`	`331`	`}`
`312`	`332`	`}`
`313`	`333`	`WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ")`
`314`	`334`	`{`
`315`		`- THEN("The class should not be marked as static")`
	`335`	`+ THEN("The class should be marked as anonymous and not static")`
`316`	`336`	`{`
`317`	`337`	`const symbolt &class_symbol =`
`318`	`338`	`new_symbol_table.lookup_ref("java::StaticInnerClass$2");`
`319`	`339`	`const java_class_typet java_class =`
`320`	`340`	`to_java_class_type(class_symbol.type);`
`321`	`341`	`REQUIRE(java_class.get_is_inner_class());`
	`342`	`+ REQUIRE(java_class.get_is_anonymous_class());`
`322`	`343`	`REQUIRE_FALSE(java_class.get_is_static_class());`
`323`	`344`	`}`
`324`	`345`	`}`
`@@ -337,6 +358,7 @@ SCENARIO(`
`337`	`358`	`to_java_class_type(class_symbol.type);`
`338`	`359`	`REQUIRE(java_class.get_is_inner_class());`
`339`	`360`	`REQUIRE_FALSE(java_class.get_is_static_class());`
	`361`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`340`	`362`	`}`
`341`	`363`	`}`
`342`	`364`	`WHEN(`
`@@ -351,6 +373,7 @@ SCENARIO(`
`351`	`373`	`to_java_class_type(class_symbol.type);`
`352`	`374`	`REQUIRE(java_class.get_is_inner_class());`
`353`	`375`	`REQUIRE_FALSE(java_class.get_is_static_class());`
	`376`	`+ REQUIRE_FALSE(java_class.get_is_anonymous_class());`
`354`	`377`	`}`
`355`	`378`	`}`
`356`	`379`	`}`