From 457bac97faddac11970351d1df639fe83e6debf4 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Thu, 28 Jun 2018 17:43:19 +0100
Subject: [PATCH 1/8] Parses InnerClasses attribute of java bytecode.

In this commit, nothing is done with the data.
---
 .../java_bytecode/java_bytecode_parser.cpp    | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 9553e3a4544..1e9306b46e2 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1640,6 +1640,48 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
     parsed_class.attribute_bootstrapmethods_read = true;
     read_bootstrapmethods_entry(parsed_class);
   }
+  else if(attribute_name == "InnerClasses")
+  {
+    u2 number_of_classes = read_u2();
+    u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
+    INVARIANT(
+      number_of_bytes_to_be_read == attribute_length,
+      "The number of bytes to be read for the InnerClasses attribute does not "
+      "match the attribute length.");
+
+    const std::function<pool_entryt &(u2)> pool_entry_lambda =
+      [this](u2 index) -> pool_entryt & { return pool_entry(index); };
+    std::function<std::string(std::string, char)> remove_separator_char =
+      [](std::string str, char ch) {
+        str.erase(std::remove(str.begin(), str.end(), ch), str.end());
+        return str;
+      };
+
+    for(int i = 0; i < number_of_classes; i++)
+    {
+      u2 inner_class_info_index = read_u2();
+      UNUSED u2 outer_class_info_index = read_u2();
+      UNUSED u2 inner_name_index = read_u2();
+      u2 inner_class_access_flags = read_u2();
+
+      if(inner_class_info_index != 0)
+      {
+        std::string inner_class_info_name =
+          class_infot(pool_entry(inner_class_info_index))
+            .get_name(pool_entry_lambda);
+        UNUSED bool is_private = inner_class_access_flags & ACC_PRIVATE;
+        UNUSED bool is_public = inner_class_access_flags & ACC_PUBLIC;
+        UNUSED bool is_protected = inner_class_access_flags & ACC_PROTECTED;
+
+        // If the original parsed class name matches the inner class name
+        // the parsed class is an inner class, so overwrite the parsed class'
+        // access information and mark it as an inner class
+        UNUSED bool is_inner_class =
+          remove_separator_char(id2string(parsed_class.name), '.') ==
+          remove_separator_char(inner_class_info_name, '/');
+      }
+    }
+  }
   else
     skip_bytes(attribute_length);
 }

From c3364557a4df837c97c612657db13a5adad83aaa Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Thu, 28 Jun 2018 17:46:59 +0100
Subject: [PATCH 2/8] Stores inner class data in java class types.

Though this data is stored, it will not be used in test-gen yet because test-gen is assuming all non-public inner classes are private.
---
 .../java_bytecode/java_bytecode_convert_class.cpp |  1 +
 jbmc/src/java_bytecode/java_bytecode_parse_tree.h |  1 +
 jbmc/src/java_bytecode/java_bytecode_parser.cpp   | 15 +++++++++++----
 jbmc/src/java_bytecode/java_types.h               | 10 ++++++++++
 src/util/irep_ids.def                             |  1 +
 5 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 9f3ff3d7744..3a74e264b55 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -268,6 +268,7 @@ void java_bytecode_convert_classt::convert(
   class_type.set(ID_interface, c.is_interface);
   class_type.set(ID_synthetic, c.is_synthetic);
   class_type.set_final(c.is_final);
+  class_type.set_is_inner_class(c.is_inner_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
index c5762137152..d663a669c63 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
+++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -212,6 +212,7 @@ class java_bytecode_parse_treet
     bool is_interface = false;
     bool is_synthetic = false;
     bool is_annotation = false;
+    bool is_inner_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
index 1e9306b46e2..9b267e30d47 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1669,16 +1669,23 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
         std::string inner_class_info_name =
           class_infot(pool_entry(inner_class_info_index))
             .get_name(pool_entry_lambda);
-        UNUSED bool is_private = inner_class_access_flags & ACC_PRIVATE;
-        UNUSED bool is_public = inner_class_access_flags & ACC_PUBLIC;
-        UNUSED bool is_protected = inner_class_access_flags & ACC_PROTECTED;
+        bool is_private = inner_class_access_flags & ACC_PRIVATE;
+        bool is_public = inner_class_access_flags & ACC_PUBLIC;
+        bool is_protected = inner_class_access_flags & ACC_PROTECTED;
 
         // If the original parsed class name matches the inner class name
         // the parsed class is an inner class, so overwrite the parsed class'
         // access information and mark it as an inner class
-        UNUSED bool is_inner_class =
+        bool is_inner_class =
           remove_separator_char(id2string(parsed_class.name), '.') ==
           remove_separator_char(inner_class_info_name, '/');
+        if(is_inner_class)
+        {
+          parsed_class.is_inner_class = is_inner_class;
+          parsed_class.is_private = is_private;
+          parsed_class.is_protected = is_protected;
+          parsed_class.is_public = is_public;
+        }
       }
     }
   }
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index ed2750317f9..1a8579f3b69 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -111,6 +111,16 @@ class java_class_typet:public class_typet
     return set(ID_access, access);
   }
 
+  const bool get_is_inner_class() const
+  {
+    return get_bool(ID_is_inner_class);
+  }
+
+  void set_is_inner_class(const bool &is_inner_class)
+  {
+    return set(ID_is_inner_class, is_inner_class);
+  }
+
   bool get_final()
   {
     return get_bool(ID_final);
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 05e84f1d9f2..a374a101b86 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -674,6 +674,7 @@ IREP_ID_ONE(interface)
 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)
 
 // 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

From b28562beaf1c706c99342e017ca9f1482f47435f Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Thu, 28 Jun 2018 18:36:47 +0100
Subject: [PATCH 3/8] Adds unit test for parsing inner classes.

---
 jbmc/unit/Makefile                            |   1 +
 .../ContainsAnonymousClass$1.class            | Bin 0 -> 491 bytes
 .../ContainsAnonymousClass$2.class            | Bin 0 -> 491 bytes
 .../ContainsAnonymousClass$3.class            | Bin 0 -> 491 bytes
 .../ContainsAnonymousClass$4.class            | Bin 0 -> 491 bytes
 ...ontainsAnonymousClass$InnerInterface.class | Bin 0 -> 251 bytes
 .../ContainsAnonymousClass.class              | Bin 0 -> 761 bytes
 .../ContainsLocalClass$1LocalClass.class      | Bin 0 -> 455 bytes
 .../ContainsLocalClass.class                  | Bin 0 -> 330 bytes
 .../InnerClasses$DefaultInnerClass.class      | Bin 0 -> 379 bytes
 .../InnerClasses$PrivateInnerClass.class      | Bin 0 -> 379 bytes
 .../InnerClasses$ProtectedInnerClass.class    | Bin 0 -> 383 bytes
 .../InnerClasses$PublicInnerClass.class       | Bin 0 -> 377 bytes
 .../java_bytecode_parser/InnerClasses.class   | Bin 0 -> 464 bytes
 .../java_bytecode_parser/InnerClasses.java    | 115 ++++++++
 ...dClass$DefaultDoublyNestedInnerClass.class | Bin 0 -> 596 bytes
 ...dClass$PrivateDoublyNestedInnerClass.class | Bin 0 -> 596 bytes
 ...lass$ProtectedDoublyNestedInnerClass.class | Bin 0 -> 600 bytes
 ...edClass$PublicDoublyNestedInnerClass.class | Bin 0 -> 594 bytes
 ...lassesDeeplyNested$SinglyNestedClass.class | Bin 0 -> 916 bytes
 .../InnerClassesDeeplyNested.class            | Bin 0 -> 309 bytes
 ...nnerClassesDefault$DefaultInnerClass.class | Bin 0 -> 422 bytes
 ...nnerClassesDefault$PrivateInnerClass.class | Bin 0 -> 422 bytes
 ...erClassesDefault$ProtectedInnerClass.class | Bin 0 -> 426 bytes
 ...InnerClassesDefault$PublicInnerClass.class | Bin 0 -> 420 bytes
 .../InnerClassesDefault.class                 | Bin 0 -> 514 bytes
 .../parse_java_attributes.cpp                 | 269 ++++++++++++++++++
 27 files changed, 385 insertions(+)
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$InnerInterface.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$DefaultInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PrivateInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$ProtectedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PublicInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$DefaultDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PrivateDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$ProtectedDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PublicDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$DefaultInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PrivateInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$ProtectedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PublicInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp

diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
index 741ff87c8ff..4c04bf031ee 100644
--- a/jbmc/unit/Makefile
+++ b/jbmc/unit/Makefile
@@ -12,6 +12,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
+       java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class
new file mode 100644
index 0000000000000000000000000000000000000000..dc41102018b2d63f74580d326c27b10a3eaa3146
GIT binary patch
literal 491
zcmZ`#T}uK%6g{J>tLvt#m01?_VBiO2L2pG6QXp786h76%xK28<&cMzZ^s{=9poe}y
zKPtMrPZ2tBzs{U<Io$7`&o2OHILO1orh^Q&;%?hU)ke+6E(4PkeTHl_m8NmRP#g5L
zinvtfN@?{r*9+4NxH0F%xsXammkjmhI#O%MVD<D^Fq8&TiMz#oB*I5N3J7r?^dj`d
zjf{tKUnvnLtA#n9@mEfgYvl*pNHw_?(NvFZ)LrD^xF}%Xg^e8fTWzm#%HaN8$>7CH
zy8%~|?)_*c{D|RbjW`kZRV2a}?vuIVf1tWr$dGQfhB&07W<Uo*itbG|0ndw#)5ItW
zaH(!k*C9sCDYZLGu=WR1ZEK12dqONyc9QQW5<er25+NygC{wjip}a#;A<Uv0zbs9A
G+1xK>)NWh=

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class
new file mode 100644
index 0000000000000000000000000000000000000000..502987e516222e87c14c67a0af7f43c3d73f5434
GIT binary patch
literal 491
zcmZ`#T}uK%6g{J>tLvt#m01?_VBiO2L~lh9QXp786u#EDPCByAz|I=<vwD!Ahkigm
zD!RK*5jt?c&YW{O-0z>yF92sa$iu>>gABIfZreuHM$N`91CtbehHNyIrg6eh8}zh_
zxK!p!Y4tYO3)2g@G3Ug&kV;0E4E5$ZQftUy_4HUUlm=3XyTyDY!bd&|2yq_tBJ{<L
zjE8bxDG?^Cg*l$_S5A^^<p<hGHMtehRF7@cUF6}oC}7`(jU4$~ZLe|4;Qn37;KfV3
z0augm{b(lqh~a3BI1%<$B*GW&leyx5pt@SfkZ!hyIHaRyKnFsK?oBoU&x?)I#3%}I
zscul$Ax6w8wL43&_6Jh!%o6GMgjl5PB;QXYenuK4LQ?QhrfQ)=d55Axm_;>yS(^5;
FxnF28Ze#!e

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class
new file mode 100644
index 0000000000000000000000000000000000000000..80d5d4a52aefce84739e342b4a1d339efb16a99d
GIT binary patch
literal 491
zcmZ`#T}uK%6g{KsuCANATA5`*4+eff2K811Aq9ffL*e`GI_bzd13PQb&+0*f9{K_O
zsOauKMd-l&I&;qDaKC>(zW`j|s00JsHVW8DyIl))3k?hV3`|fA8O&rRbnA?vF&ZeD
z_(JL%spQ*2E%hMswZ0_Im5?I2W@xrIkvd}rW1uFS!5s<7AC`-N$IpHc5n?~7WgPN5
zkq*_NlswK>bA3AZUwx9?$}mz|$mu;#W@=)g>7WGLK^cb*EELJ#dV8&N2Iuce1}|OO
zk9;}pKL&FiCJZMV#F=m?6CS_#A(^ZE2kPsE4Ec6vjAJ@#0dyeb=-y-#@VwMGO^l)p
zhw2t}Jz}IBx7%BRbw7~nnk(erGh&6ZoqY!+4v~jTNDdyVR1MT9?@`nUGpMG|r0Kvc
F{sL-_ZfpPm

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class
new file mode 100644
index 0000000000000000000000000000000000000000..d215c74a240e7a022305a6c58c951d81ab80bb43
GIT binary patch
literal 491
zcmZ`#T}uK%6g{J>tLvt#m01?_px_5&555&aNP%GWQ20KsqmHaIu(JmJtR5ujp&!tX
zitg@Hgbv)VGv{0m_xtDb3qT)dd05zYkikLR9onecsM$DXV3K0Ukc}47G%guxqk&ct
zm&)8Kt=?98Z3Y21=88DiQpxCsq2Ag>YL6MLfu0J6(nu=txL!>}_`)XvA<na2hrYO%
z@lYNrCBkI2Fc(Yy%1Lsk{6HJ2<_{uT=&6mmi#!|`1)RFDkt2WG?KS!g?%$ORUc9sy
za5e8eO_sus7@9l8iEyYQ5ze?z=8FG;>UJSRy44=zoQ|3S9SAA9H`xR{FE&mSqbR_o
zx<_4?7%`{R>2AO}A4qlV4btxku}IlTz6FVANTWnZ3LeT-EmSBUQB(-CsKzf#(@8e>
E3vBCdbN~PV

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$InnerInterface.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$InnerInterface.class
new file mode 100644
index 0000000000000000000000000000000000000000..6914c2338dbc8e8d5c7a836106d4db1bdb3ac21e
GIT binary patch
literal 251
zcmZur%L;-}5Iv)nX4+#Dw6AS$`hgGvS1p3}H@SskBY3Ytzt*A;=%b?1RYZ$9!<qA7
zUhl^fzy=c!frp4dxlBrkl8TL0Y>%pJv@0eMf<x8Rncn54Cd^W1T_>e7Mw@k^Zpy=$
zu#%uvIh!q4e7{zW=`736owC*SS!EI*{~p5cKEkwZj7!Crcz-H%W(o8E)r0mmr+aV#
Y7d>HpVGcwP^g8qr$__*$3^5w`A6FYaU;qFB

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..eafeaf17b03d479bda2e694ada5f9a3fc7396333
GIT binary patch
literal 761
zcmaJ<*-FDe6g?B$rp9Pnm%8s&+bW9NQ$>)9Acz(eQBY)3M~TD<WD)!<ABv#h2l!Fq
zokU9&>p*hOU32c_zJI*D0ocHjfea>eOd8NI)rlTV>zFZ+jEz|x1q12WnA0(Dper^O
zbQE=zbd(u-_N5fwz6^wS!|Q^<j2u;m`@ZlQGF-ay@!k#nT4*_Tonhgi>dJuI(%<<G
zMcIX)ohl63X6>%H;h_^S^fp~J&kaO95ZA4FHP3$F0jWrB+0qWS89IukQ-(y<y(Vww
zz?R}LytjmR!Yzk9#<3fEb+KnFBiAZ@`Hnwu6GIqg7;2+<RmB%g^r63f(wd2Z|KjT=
z^8dv*Obn`c{%;X9zEZm4aCy6OWZlu7FwFg(`|FAsMvHBJMx}I$DcXn(ZAt=6O-KxC
zlE_1f2{omRkkLaIML0t2GO7SJ%g<otS7_%%IvPk2Pb!{jKqsD7yt4s=c$ea41Km$i
xyHR@QX%T@lYIcDvt}q4*MF{%n82L4fqnEHuSy>XAOQmT&<CFeERj-Z~!zbMJvakRE

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..2d58f305b14249e0e7e16af233ccffb9c29b817f
GIT binary patch
literal 455
zcmZutO;5r=5Pi#6rB*2jii(B<2dIf?Vq%QO3(<rG^`PNi$_AE{tznD*%L6g-;1BRe
z8DF_bf`^%TGyCSv?0o-xegU|^Q63rW*vO)spo)cE3;O~>(YgY;c&tq0OrYHBL^}4B
zHoYkD!%pZMbItb~rB!?@P;LH4=(hR-nNBp60)?K^@^L;L$k~fO2wAb8qxme5_bN$>
zU9IJ8sVmLt#DDYIa;JkZGD?pgWIT?B77iR7qUK-&c?Wiaa<BxB*OzOY|1HW<tBJEZ
zO2AEqwL@Qz+E0Ut3}S)Ox*q=#OT)Kxv(-nP$I9}8DH=BbTsPT?nV{L&WORtG$Vf9*
zypsil_kon>UM`UKYIN^Q`WAhOa)7456a_>m<CSgOtfiQ{j2RTksuJ0hPS|_EFM^C-
Axc~qF

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..40be03e68ea3488f54c02281c5ac77a4ffb21549
GIT binary patch
literal 330
zcmZWkO>4qH5PcJ)(HK8(JybmOV0)+t9!oEQf*|d|()%V|%7%0UN%Vht5<K(=^hZfw
za%iP4?7W#bZ{F^FpN?MumKghJpzmSeVd!Bb@Yh+a(lAv;AqZC1>bx#A%hrRjrhF7M
zX18wwH_YC(V6Zk;KW{%HoxiFmCF7R5C~39Hwt1|dOvR1Pt?m=GQvp1*1>-QYr82fS
ze|T64=BctD^Oq>mG2JGYx|_w{45o0nN_8AwT0_ubc1;vw^X>rIGvUV=TQ!+5c7LT;
Xb(f0&vYeg)n+|#$1P!<(u?hSD#lApA

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$DefaultInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$DefaultInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..4170d0b67a9840391b71589ac2d534398057614d
GIT binary patch
literal 379
zcmZutO-sW-6r7i&joq$ETD2;Oc<7-`!Fcedc&P}1q6ek-O<i?MOd%isFAqiV;1BRe
zi7&mhf`{2RZ{F<e$M?_Y7l3mdw%{NTXrNQGu8Un4`vfwKn9wX=Owm6hc#}BGbUsd1
zQRw1=CzmEO<rSej_&bV+Q-U*IJZgeJF`2%tUK5=^s3c`Y+%Kwprf*E$bT%_j=ju&K
zY@sC~a3Ily>!L?E-gNb^^^>a7a;<U9Kbl+{bU_H}@F-Q;b99%?^{gb=gW(h>{OAV%
zgvH?VfFP)Ez#TCJ+FT{Gh#fXpKO8MV;RmenXbJm$W!&b~Ta5*8Z8Mi__gJ;yqsLWn
JjDsEQ0lyA^O0fU{

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PrivateInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PrivateInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..b17f91da63cb617d4f7a36c705937ba3ce91cbcc
GIT binary patch
literal 379
zcmZutO-sW-6r7i&jg2u$tELr1JoL~;Fdn=qUJ62>sG#(|sf%ujTgayUUml9!!5`p{
z5?^|01zC3Iy_wnBkMEz)F94S~YQaI|p@DW?bzB^{=n_cr%m~fuRhj+;AsA;`%W_l*
zW2Cua<yvV~-4Hs1zfv}w5S-EcSrWpr((-Qcmdo-<<OMU{<9tz0<*lll_IBp^Oe}?u
z9khIS==o^EbrBOzwq5;)QY}R#Hyp?O!}%M7G=!)QPYa=6())ZSrxn2-3@13{M>qH<
zEFOFw5JmM3m?367>@xb?rQF$!VRE(tB_FVo;}z`pwQ-NvU@gbIwaayn?E$kELd1+7
K$2i!>A*^3C0ZRt}

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$ProtectedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$ProtectedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..7a8ae4aefa32267eaf3516b8287f1dbe94a19cb8
GIT binary patch
literal 383
zcmZutO-sW-5Pg%Rjg2v1)vDk@p@%jF<H4Kar62@~3QF%uyXcm<fh6^Rc_=~;{($}{
zags|bc-Vb2Z{EI{+0D=T8^ASAJ22o`Xu+?ez{H`6V**J&F`-?($+CY%a3--*q8MjM
zS&H(8E4Na~>W&Z${+8n5lwgeWxgfX`sl>zbJr%`El4i_U&-t>LiF;Wm{;uccBKb&c
z?4e`B!ikMGOcOoA`L3$}ROFSIRbswn3Eh8Ldn*wo!K)iYS)yK}$8^CS1br}^;(`}%
z@o#91+!OG;dJ1NE4<2Qo(dH~-h0f@PqZKIpf)<{wpno>P1HPT6?D12d<ACK3vl?9V
L7_G*xiz67nArDNR

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PublicInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PublicInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..a5f5c2b47c355bc340425d2bda64634a6769ab7d
GIT binary patch
literal 377
zcmZWl%SyvQ6g@Xj8)K4ItqQsjx@c1{F5D?@3PPZ$pmaZpgHDMlWD@_&MG;*10e+Nt
z(@iTb=046j_srb+{`vd@aDk%^EJPk`bla-uV$a0^ffS#V;M6Zl56%g}G%ZV6O$wp4
z)R)X$sZ!O~gx>Hkm5ycvYqEHfgm9`#dE2~ZvU(I*!HD;;XsTS^sJ7{DdY;Y2oA9xP
zjt>uqJ{-6%`h=5B)!@F#3YD)RLi8W<*SyrMXswe%l+VdsHkWx#Fo&ZVPI+aU|G@z7
z0~d&*_I^fqdw#?=N1wZd6(;8}9xp-h2aNc53G;m=+~F9kXp2W}t{s*Kj2Z~h=j^eK
Jg<b4}egPc9N!0)V

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.class
new file mode 100644
index 0000000000000000000000000000000000000000..0d9ad31914f7cb29dd7aebecfcd289591f14f5d6
GIT binary patch
literal 464
zcmZutJx{|h5Pg@nF@!)H%I8o7r~@$2g%Pn7At51%1Y&p61Gx%`<RtxHOh^p;0DctW
z(j_Iur@QlecRu_1`{(luzy<a_w9r>@6}A+%2|;MhOc#8crfkQF&U1oa1I`t82>sAz
z1;+(X>XO2)9KYrlT_(jMy+`PUWt5n>W(n@4NlkG@Xq}us6WZf!!i4UfN%_8fi`YKt
zC=tec%t{;cjj2FTPvHD~s%P5AIyU5jYClSJ`Z{`urt&hv!D8?5A6bWuh9yPK8B5v-
zgTFHxDscoy{<m5rCNGuP6*QP*pmX*CdY_kj5?!IIRtJG(2b;nG$7qW==!h%v6+x?#
KJ*llp_Cdd7)pBeA

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java
new file mode 100644
index 00000000000..7b4792fa26a
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java
@@ -0,0 +1,115 @@
+public class InnerClasses {
+    public class PublicInnerClass {
+        public int i;
+        public PublicInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    class DefaultInnerClass {
+        int i;
+        DefaultInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    protected class ProtectedInnerClass {
+        protected int i;
+        protected ProtectedInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    private class PrivateInnerClass {
+        private int i;
+        private PrivateInnerClass(int i) {
+            this.i = i;
+        }
+    }
+}
+
+class InnerClassesDefault {
+    public class PublicInnerClass {
+        public int i;
+        public PublicInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    class DefaultInnerClass {
+        int i;
+        DefaultInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    protected class ProtectedInnerClass {
+        protected int i;
+        protected ProtectedInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    private class PrivateInnerClass {
+        private int i;
+        private PrivateInnerClass(int i) {
+            this.i = i;
+        }
+    }
+}
+
+class InnerClassesDeeplyNested {
+    class SinglyNestedClass {
+        int i;
+        SinglyNestedClass(int i) {
+            this.i = i;
+        }
+        public class PublicDoublyNestedInnerClass {
+            public int i;
+            public PublicDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        class DefaultDoublyNestedInnerClass {
+            int i;
+            DefaultDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        protected class ProtectedDoublyNestedInnerClass {
+            protected int i;
+            protected ProtectedDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        private class PrivateDoublyNestedInnerClass {
+            private int i;
+            private PrivateDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+    }
+}
+
+class ContainsAnonymousClass {
+    interface InnerInterface {
+        int i = 0;
+    }
+    public InnerInterface anonymousPublic = new InnerInterface() {
+        int i = 1;
+    };
+    InnerInterface anonymousDefault = new InnerInterface() {
+        int i = 2;
+    };
+    protected InnerInterface anonymousProtected = new InnerInterface() {
+        int i = 3;
+    };
+    private InnerInterface anonymousPrivate = new InnerInterface() {
+        int i = 4;
+    };
+}
+
+class ContainsLocalClass {
+    public void test() {
+        class LocalClass {
+            int i = 55;
+            LocalClass(int i) {
+                this.i = i;
+            }
+        }
+    }
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$DefaultDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$DefaultDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..55ee343fcc8705e2164dd776cf47b0e1eb2db2b9
GIT binary patch
literal 596
zcmb7BO-lk{5Prt5O<Q%fFDr!(d$29Cpj**Jvjnk&(S27Zdu3b0-3|I#9VF<`59mil
zvw|o@Mu&Old1jtxnBo2Wdj9}$ib@&@tYwhIdW1GKY-%VGNJ+E^so+8R=81+KLZPd?
zf&0>7Kj41dwSAwUw>*!>Q^G<I+l#!x{4~>>Kg?$`{akq}xF8%?|6^?J-w_h^QJ)F<
zw(__WJ~}+UwH;R~neHeY_qeGdQdr#QXlOs%I#!_T$YNJV3L4>hQL=nxv%&Xv=mw2Z
z=*$kAy9t#)`bM-s&9%Kj?Zz2$FVIjXSo0C=FJFKVuSUn0ezRatelaOu8<UXp0K<q5
z7Df_T<Rs?>)kG1OoVN}pAnOe=t2{ycbt*LE%}v{vNTVtEO5_Ep#!$qn<f5Q7wviE>
I5VQq+1K_rrQvd(}

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PrivateDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PrivateDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..07f49f71e4493b0e8521376dbf2c1ca4fc3af3ff
GIT binary patch
literal 596
zcmb7B+e!ja6kU6~OxmcU-K-RP@WH0Yg5HW=lt>V}7`@Nv#*R#5%#1>x)q?~*^Z|WT
zv_}wy$cV!^d#!zAEzalH`v-tilv9XfEsX@$BebDoQ%8|NN^X;o3?EfcInl90$aj?2
zcVF5ZgxssUb`TJZrsuIgB`ox?wa6RH&$Ir@kKr@fey%(fUJ#C}{~2uVKM>;eVUG#9
zmh!kgdUDvmw;fk9>CSNEcllC9B)_QVXkd?R11m5LWUy->37v4Y*s@%5<;GWIJLJZ2
z<jjoCrwQdh>SiRM=GtDrcI^zf8|o+#toaHKmJ1-ns*(BPZzI@~Urfl?YI4LLV49I(
z$&h3+$V$u!s|kxq%vlE$ko5-5Doqf3oi>{CW~b#_q;My=Bkg&~YA9e;VnI*}+eizJ
I3)+JA4Hi$DsQ>@~

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$ProtectedDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$ProtectedDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..3e31610669599cf59a0643d5960109888caf980a
GIT binary patch
literal 600
zcmb7BO-sW-5Pj38jft^M>sQr^2tCv&R>7O%rA3IwDpb5D?NYbIM3PkSXL%@s2Y-M+
zN}Lo*3u48??z}hqW|%ko`Stz*-~`(m6fEn=VI@VYD%Mm~2qgK~gnaTK<Jz%`O+u+7
zgTDXL7I7kaP2Y`Uf?)@Nh{i-PJ#c1uONgh5zV@T|l)InFKqlveqxyde?Y(<~(hPfo
zP;_J<+QUarM0c*|b4Krk!>B7RWJ*f2^BfM`XV<_23<FEpGLVN#xSW;DAGvlLg^B30
z{Z=^iCf26)gq=SXW;#T}cY}W8#v5=m6;*;YZ6f0NLlCm{bODv$O0dg6nd9%xaAb>s
zX{M$*!)s&b1&&2#4OV117Onje$a+J@s*aF-9Scpq3*+Z2XmA)`v%JLF49ZyKSZ1VQ
L13F`c(K?iGR|K3u

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PublicDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PublicDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..269291980506dd232b3fa059261a702c51cc4ecb
GIT binary patch
literal 594
zcmb7B%Syvg5Ixhhjjgds>#J&A2wBu9M!}upgBB%Fs!(yCw3qglm`IZdewK?OxbOq~
zC~;Dh7Q}*!d*__FXXei1<MZtuz%jN9$YQyO99B}as$xw=l|Yh@L&(Pi8JR~aHVNg9
z4Ep|aTST$wHGDUU2$~ZFVl*Lw>3(aLH-&io(VM@5PdNLj3}k#pIIRCC(Am8wWE){m
z5cHM|L_2x##OTiTeD)MOVKVB9E18n=Y&{1<_sP|;08PUZwlw6S60T<@^Gh~w6VI33
zX2|Ay4%1*lZT_>7esBA3(6?{Aq3FgcY6NSVK}7SvCn)u__3B?C*x?=Kc(EDqaG?T*
zk+#boUMKfl;#+5CvqE93TYF=W^@@yD8$)@S2o1hVljn03aKZSJ<z@C}P{AVG3Znux
LP-L8Cv<~_LMT41l

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..0baab8760494e499ff60a62d3aefffa685db754f
GIT binary patch
literal 916
zcmb7DO;5r=5Pic}1*?FfB7&fz!J3E%PeQyvR1859jQ0X7E~&+|g~XrbftYyk2l%6m
zQxXCPAaZy+GrO;ECi}KOzhB<~E^!is4~Y=`*mJX_f_(*PLbM^xj`3a-wj<glL$_^$
zS}{#wjS68a$PiL>OAd5LlzaW=m^>jVI3T3!R?iVFR+&dSWSz2j*87Gtk8(sv*13gj
z&1MitGAe|C^CIo+1tC$L3?l5Z5O3oF3(P7?Q##j#{oH(7<@AZ*EA`rf5Uxs7)cUVY
zVLj?igLguWUf*ho8|fC&>0akueW0t@z@~~AvMM5oDmW%+)2!)<vNJ9_;;Q5g-R$Ha
znq9s?!rlMB&n`5EaKDt)LIanZYoXDE+hyij_#nJF*S`2XJ!JT``}r5}FxVhoBCcgz
z5hI2zj@z8&nc?La*3O0??Gqj?IfVCPMBL$ZeRO<<APSrpnI7j|4|bt&)VPTcDFirQ
U;Vj4}A&#pIm9aKb@F5KP1D3xBUH||9

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested.class
new file mode 100644
index 0000000000000000000000000000000000000000..38ae4c2b9cbd744ec36e284a288eb2a171ef79bb
GIT binary patch
literal 309
zcmX^0Z`VEs1_l!bK`sVn23~dsK6VCvb_M}P2EpLWy!4z(ztrNA)D-8O#NuK`1|HA6
zywoBvCl$zLv&qcMEU{x`VAjwKV`N})&QD2YWZ?J7%uDqv%}q)z3Q0`L0g7-1=a&{G
zr@Cc=ID*J#=w&6ACGs$^GjK36NFYnNq^1_YEN5g804dYYNz6;v_fN`7O)g<%(88r!
z1;gD83Jgp@&w&6V5Cbg((wsn+ERY6?uxf2*VB83n<^qyzU_o=BCT<{)iGc?w!oa`<
L6lDSOSQ!`qLvu%c

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$DefaultInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$DefaultInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..963ceb186cf80cdcf27a5250f0de7eb7b9a2f9ea
GIT binary patch
literal 422
zcmZvY%TB^j5QhJ03zb@F5m7NNTmWK8tP6J<HyD#9L>C(Or+CyuYDs$Wy;u+v7e0Uw
zWt@^GbircI+`cpOXMX>_e*j$Kr~w16g&JB#v}<C|!~ua6TR^C1?<(zG5IU0}j%6~A
zM4HO<R=$cn%B~o=R<X)%2;JdEA~<^{7~}biBsdcl%lrHzl*y9_Bd%DF^E{c#J5?mD
z>W1@~_!Ks_(6C|Q&_*4mi7ugErAi&W(yv=QZ9~mo12QGJ#ST9b@tgk;&g3*B=)*#9
zyULYwaKiVg@zFFk76Z6$A&)a+v#`zH=E!G4XYY8UCCK}N<{dAgFIM0Vzs*&<&tC@|
UpEBO$ss;!9>@6N+pp6dj53JH#4FCWD

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PrivateInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PrivateInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..6961af273b846495dea676ae7b557b2f40db5d81
GIT binary patch
literal 422
zcmZutO-sW-5Pg%Rjg7HMtyL=?JXEMDG=AL_FBKtBR8YKc>T0*d6!Ovk<)H{3`~m(b
zaZ(D+p)9*^=FQug$Nc_%{{XneK@A363l%hqXxqe&i9G@-z5$_{jaAw?CA5Y?9Lr=7
zi8Phzt$Y)ClwGmlTE!~6A+)<|6~W01!5B<mCBYf0Sl;I!p-i4d7%^i#P4i?V?^KaA
z$`kq%F%vd6P_toS-$oUti8kT5tXlf$JSJ);GPx>ow>6x-63CR`7Bl=v#P9w?IFX}_
zpmz(u&9ZJe14q1{3NKCL!)5^2E$lHv%vjiDv^n!R(-|GFHwSrN(7eMr^v{KGi{JX9
Ze8ykTIlf?dommYIb{Q>hW1xu^w13tdTVntK

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$ProtectedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$ProtectedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..80306a39a3335650fca781864190a724d8df07bd
GIT binary patch
literal 426
zcmZutO-sW-5Pg%Rjg7HMja4gNgn~6y<H4Kar6L513X1onU3E*EKtB9m9*W?>AK;G?
zC!x?Bdf0t4Z{E(lo!`Ij9{`s)XhDN*pn*;qZR^<4u}2`u$0s!NcbWAs2;H$C$08j?
zL6(W^R=fs9lwYynTE;TJA@l}o75>Q!K^rAgL9oU$7Wc(G6zOviM$8ybNs&&(oh*}1
zeZu)H_y|mFpk>0qzKJGu9X-NvUA6Sle@v5HOmZ<@6$#E-)?7(MMzG5{UKGS{-a|O!
z9t3qzdUoo%<s2OGjvBl;g^>*bwq06ehCj(ZHyKUNJXWZTmOEU4+%G8Z;R5PsCEVh>
aU6qIY^pxW>mbaNzU}2ZhsM<N`Li+~@(_H!h

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PublicInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PublicInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..77340e82c70f52f59dd769102406f52845466dbe
GIT binary patch
literal 420
zcmZvY%SyvQ6o&tkq>YWSNv%~Yf)=u<5sV9WikpfMC@LuKCvns%X$racUM`B@!Uyo7
z#FJ8JKo@ha-^}^veE)oY0XV~63kF;Z4Roq#)5MmE9RevnA)#5ks@yvz^u}SD%50Q~
zJeT>Ed=_O=oHKBtQdL|M`on*T@aU0XjAl=g;EYu&Z^~&Tvj-6+T(RzFWfse8RVAJJ
zgp-MQ6E@b+vSDG@MiZuqKEbO~OC8=_86_%SbqMa?lD+E7oQY~ekcjjpxQ!+<E(rRt
zQroR_%Ly3pb{f1g4g6=Afa_M`xWbEKh3jl>&H^TM_Ktr%2l*e+{QWuf_XW7Yw!LT{
Y@YO?(2aLD5s=>iFdyAhj&_xgQ3z&*pF#rGn

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault.class
new file mode 100644
index 0000000000000000000000000000000000000000..fd18bd4c3c538a5fe5406aa47ec18df5188cd580
GIT binary patch
literal 514
zcmZ`$OH0E*5dJ28tj1^?>l+1;ijRZ6coZ)cK@bfn-Z$weTjB=t=>PI0c<=}Kqr^!O
zQf%C1c6PpRW_D)w>-*yqz&UnYG|*F6Q&?BnAoxLQCOYREYdIapI?D)NWpJjjN$3S>
zl5>>vsG=0MB>ak>brI*Y@HU|v6k%+l3MI5Jj5YZsp>cfjL}(6^5feJM#`0b98glxm
z!&ngaAt};`uT5$ARR+$^#(JVXEMr9qnk9Z~kY`JeL9Fe|;65Bny@bOW$9_%ENA-Sl
zUH_ADZVZHeZN@)y!9E=Mk#doU^d`C^w>{A%(mH(yy-n$^ob4&ND?z?k4ps#L4$zeC
Tpe3S27Q|W<?FzRf+5`On395x`

literal 0
HcmV?d00001

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
new file mode 100644
index 00000000000..6866b177c6e
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
@@ -0,0 +1,269 @@
+/*******************************************************************\
+
+ Module: Unit tests for converting annotations
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java-testing-utils/load_java_class.h>
+#include <java_bytecode/java_bytecode_convert_class.h>
+#include <java_bytecode/java_bytecode_parse_tree.h>
+#include <java_bytecode/java_types.h>
+#include <testing-utils/catch.hpp>
+
+SCENARIO(
+  "java_bytecode_parse_attributes",
+  "[core][java_bytecode][java_bytecode_parser]")
+{
+  GIVEN("Some public class files in the class path with inner classes")
+  {
+    const symbol_tablet &new_symbol_table =
+      load_java_class("InnerClasses", "./java_bytecode/java_bytecode_parser");
+    WHEN("Parsing the InnerClasses attribute for a public inner class")
+    {
+      THEN("The class should be marked as public")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_public);
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a package private inner class")
+    {
+      THEN("The class should be marked as default")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a protected inner class")
+    {
+      THEN("The class should be marked as protected")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_protected);
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a private inner class")
+    {
+      THEN("The class should be marked as private")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+  GIVEN("Some package-private class files in the class path with inner classes")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "InnerClassesDefault", "./java_bytecode/java_bytecode_parser");
+    WHEN("Parsing the InnerClasses attribute for a public inner class")
+    {
+      THEN("The class should be marked as public")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDefault$PublicInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_public);
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a package private inner class")
+    {
+      THEN("The class should be marked as default")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDefault$DefaultInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a protected inner class")
+    {
+      THEN("The class should be marked as protected")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDefault$ProtectedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_protected);
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a private inner class")
+    {
+      THEN("The class should be marked as private")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDefault$PrivateInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+
+  GIVEN(
+    "Some package-private class files in the class path with deeply nested "
+    "inner classes")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "InnerClassesDeeplyNested", "./java_bytecode/java_bytecode_parser");
+    WHEN(
+      "Parsing the InnerClasses attribute for a public doubly-nested inner "
+      "class")
+    {
+      THEN("The class should be marked as public")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "PublicDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_public);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private doubly-nested "
+      "inner class")
+    {
+      THEN("The class should be marked as default")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "DefaultDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a protected doubly-nested inner "
+      "class")
+    {
+      THEN("The class should be marked as protected")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "ProtectedDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_protected);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a private doubly-nested inner "
+      "class")
+    {
+      THEN("The class should be marked as private")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "PrivateDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+
+  GIVEN(
+    "Some package-private class files in the class path with anonymous classes")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "ContainsAnonymousClass", "./java_bytecode/java_bytecode_parser");
+    WHEN("Parsing the InnerClasses attribute for a public anonymous class")
+    {
+      THEN("The class should be marked as public")
+      {
+        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_FALSE(java_class.get_is_inner_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")
+      {
+        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_FALSE(java_class.get_is_inner_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")
+      {
+        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_FALSE(java_class.get_is_inner_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")
+      {
+        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_FALSE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+
+  GIVEN(
+    "Some package-private class files in the class path with local classes ")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "ContainsLocalClass", "./java_bytecode/java_bytecode_parser");
+    WHEN("Parsing the InnerClasses attribute for a package-private class ")
+    {
+      THEN("The class should be marked as package-private")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::ContainsLocalClass$1LocalClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+}

From 1930aef72009953af3ab9ca9cd4026a747a4ec18 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Mon, 2 Jul 2018 12:28:30 +0100
Subject: [PATCH 4/8] Refactors parsing of inner classes attribute.

---
 .../java_bytecode/java_bytecode_parser.cpp    | 112 +++++++++++-------
 1 file changed, 66 insertions(+), 46 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 9b267e30d47..817c0f05378 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -119,6 +119,8 @@ class java_bytecode_parsert:public parsert
   void rfields(classt &parsed_class);
   void rmethods(classt &parsed_class);
   void rmethod(classt &parsed_class);
+  void
+  rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length);
   void rclass_attribute(classt &parsed_class);
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
@@ -1576,6 +1578,68 @@ void java_bytecode_parsert::relement_value_pair(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.6
+/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6
+/// Parses the bytes of the InnerClasses attribute for the current parsed class,
+/// which contains any array of information about inner classes. We are
+/// interested in getting information only for inner classes, which is
+/// determined by checking if the parsed class matches any of the inner classes
+/// in its inner class array. If the parsed class is not an inner class, then it
+/// is ignored. When a parsed class is an inner class, the accessibility
+/// information for the parsed class is overwritten, and the parsed class is
+/// marked as an inner class.
+void java_bytecode_parsert::rinner_classes_attribute(
+  classt &parsed_class,
+  const u4 &attribute_length)
+{
+  u2 number_of_classes = read_u2();
+  u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
+  INVARIANT(
+    number_of_bytes_to_be_read == attribute_length,
+    "The number of bytes to be read for the InnerClasses attribute does not "
+    "match the attribute length.");
+
+  const auto pool_entry_lambda = [this](u2 index) -> pool_entryt & {
+    return pool_entry(index);
+  };
+  const auto remove_separator_char = [](std::string str, char ch) {
+    str.erase(std::remove(str.begin(), str.end(), ch), str.end());
+    return str;
+  };
+
+  for(int i = 0; i < number_of_classes; i++)
+  {
+    u2 inner_class_info_index = read_u2();
+    UNUSED u2 outer_class_info_index = read_u2();
+    UNUSED u2 inner_name_index = read_u2();
+    u2 inner_class_access_flags = read_u2();
+
+    if(inner_class_info_index == 0)
+      continue;
+
+    std::string inner_class_info_name =
+      class_infot(pool_entry(inner_class_info_index))
+        .get_name(pool_entry_lambda);
+    bool is_private = inner_class_access_flags & ACC_PRIVATE;
+    bool is_public = inner_class_access_flags & ACC_PUBLIC;
+    bool is_protected = inner_class_access_flags & ACC_PROTECTED;
+
+    // If the original parsed class name matches the inner class name,
+    // the parsed class is an inner class, so overwrite the parsed class'
+    // access information and mark it as an inner class
+    parsed_class.is_inner_class =
+      remove_separator_char(id2string(parsed_class.name), '.') ==
+      remove_separator_char(inner_class_info_name, '/');
+    if(parsed_class.is_inner_class)
+    {
+      parsed_class.is_private = is_private;
+      parsed_class.is_protected = is_protected;
+      parsed_class.is_public = is_public;
+    }
+  }
+}
+
 void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
 {
   u2 attribute_name_index=read_u2();
@@ -1642,52 +1706,8 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
   }
   else if(attribute_name == "InnerClasses")
   {
-    u2 number_of_classes = read_u2();
-    u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
-    INVARIANT(
-      number_of_bytes_to_be_read == attribute_length,
-      "The number of bytes to be read for the InnerClasses attribute does not "
-      "match the attribute length.");
-
-    const std::function<pool_entryt &(u2)> pool_entry_lambda =
-      [this](u2 index) -> pool_entryt & { return pool_entry(index); };
-    std::function<std::string(std::string, char)> remove_separator_char =
-      [](std::string str, char ch) {
-        str.erase(std::remove(str.begin(), str.end(), ch), str.end());
-        return str;
-      };
-
-    for(int i = 0; i < number_of_classes; i++)
-    {
-      u2 inner_class_info_index = read_u2();
-      UNUSED u2 outer_class_info_index = read_u2();
-      UNUSED u2 inner_name_index = read_u2();
-      u2 inner_class_access_flags = read_u2();
-
-      if(inner_class_info_index != 0)
-      {
-        std::string inner_class_info_name =
-          class_infot(pool_entry(inner_class_info_index))
-            .get_name(pool_entry_lambda);
-        bool is_private = inner_class_access_flags & ACC_PRIVATE;
-        bool is_public = inner_class_access_flags & ACC_PUBLIC;
-        bool is_protected = inner_class_access_flags & ACC_PROTECTED;
-
-        // If the original parsed class name matches the inner class name
-        // the parsed class is an inner class, so overwrite the parsed class'
-        // access information and mark it as an inner class
-        bool is_inner_class =
-          remove_separator_char(id2string(parsed_class.name), '.') ==
-          remove_separator_char(inner_class_info_name, '/');
-        if(is_inner_class)
-        {
-          parsed_class.is_inner_class = is_inner_class;
-          parsed_class.is_private = is_private;
-          parsed_class.is_protected = is_protected;
-          parsed_class.is_public = is_public;
-        }
-      }
-    }
+    java_bytecode_parsert::rinner_classes_attribute(
+      parsed_class, attribute_length);
   }
   else
     skip_bytes(attribute_length);

From c0c1029208a62433a3803b5aebc727337b22b31c Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Mon, 2 Jul 2018 16:40:19 +0100
Subject: [PATCH 5/8] Fixes parsing for anonymous classes

---
 jbmc/src/java_bytecode/java_bytecode_parser.cpp | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 817c0f05378..99ff7f2c77d 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1588,7 +1588,8 @@ void java_bytecode_parsert::relement_value_pair(
 /// in its inner class array. If the parsed class is not an inner class, then it
 /// is ignored. When a parsed class is an inner class, the accessibility
 /// information for the parsed class is overwritten, and the parsed class is
-/// marked as an inner class.
+/// marked as an inner class. Note that is outer_class_info_index == 0, the
+/// inner class is an anonymous or local class, and is treated as private.
 void java_bytecode_parsert::rinner_classes_attribute(
   classt &parsed_class,
   const u4 &attribute_length)
@@ -1631,7 +1632,17 @@ void java_bytecode_parsert::rinner_classes_attribute(
     parsed_class.is_inner_class =
       remove_separator_char(id2string(parsed_class.name), '.') ==
       remove_separator_char(inner_class_info_name, '/');
-    if(parsed_class.is_inner_class)
+    if(!parsed_class.is_inner_class)
+      continue;
+    if(outer_class_info_index == 0)
+    {
+      // This is a marker for an anonymous or local class
+      // which are treated as private
+      parsed_class.is_private = true;
+      parsed_class.is_protected = false;
+      parsed_class.is_public = false;
+    }
+    else
     {
       parsed_class.is_private = is_private;
       parsed_class.is_protected = is_protected;

From 6ce7b1331c764d34c18f3402cfb27e0d58947c88 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Tue, 3 Jul 2018 12:23:45 +0100
Subject: [PATCH 6/8] Clarifies language in documentation.

---
 jbmc/src/java_bytecode/java_bytecode_parser.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 99ff7f2c77d..05307e0a539 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1581,19 +1581,19 @@ void java_bytecode_parsert::relement_value_pair(
 /// Corresponds to the element_value structure
 /// Described in Java 8 specification 4.7.6
 /// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6
-/// Parses the bytes of the InnerClasses attribute for the current parsed class,
-/// which contains any array of information about inner classes. We are
+/// Parses the InnerClasses attribute for the current parsed class,
+/// which contains an array of information about its inner classes. We are
 /// interested in getting information only for inner classes, which is
 /// determined by checking if the parsed class matches any of the inner classes
 /// in its inner class array. If the parsed class is not an inner class, then it
 /// is ignored. When a parsed class is an inner class, the accessibility
 /// information for the parsed class is overwritten, and the parsed class is
-/// marked as an inner class. Note that is outer_class_info_index == 0, the
-/// inner class is an anonymous or local class, and is treated as private.
+/// marked as an inner class.
 void java_bytecode_parsert::rinner_classes_attribute(
   classt &parsed_class,
   const u4 &attribute_length)
 {
+  std::string name = parsed_class.name.c_str();
   u2 number_of_classes = read_u2();
   u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
   INVARIANT(
@@ -1634,6 +1634,8 @@ void java_bytecode_parsert::rinner_classes_attribute(
       remove_separator_char(inner_class_info_name, '/');
     if(!parsed_class.is_inner_class)
       continue;
+    // 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)
     {
       // This is a marker for an anonymous or local class

From 9ba55e20aad17e94ac1fa6873681c20b3e3194c1 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Tue, 3 Jul 2018 16:42:38 +0100
Subject: [PATCH 7/8] Marks anonymous classes as inner classes

---
 jbmc/src/java_bytecode/java_bytecode_parser.cpp       | 11 +++++------
 .../java_bytecode_parser/parse_java_attributes.cpp    |  8 ++++----
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 05307e0a539..a1e749d11e8 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1628,18 +1628,17 @@ void java_bytecode_parsert::rinner_classes_attribute(
 
     // If the original parsed class name matches the inner class name,
     // the parsed class is an inner class, so overwrite the parsed class'
-    // access information and mark it as an inner class
-    parsed_class.is_inner_class =
-      remove_separator_char(id2string(parsed_class.name), '.') ==
+    // access information and mark it as an inner class.
+    bool is_inner_class = remove_separator_char(id2string(parsed_class.name), '.') ==
       remove_separator_char(inner_class_info_name, '/');
-    if(!parsed_class.is_inner_class)
+    if(is_inner_class)
+      parsed_class.is_inner_class = is_inner_class;
+    if(!is_inner_class)
       continue;
     // 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)
     {
-      // This is a marker for an anonymous or local class
-      // which are treated as private
       parsed_class.is_private = true;
       parsed_class.is_protected = false;
       parsed_class.is_public = false;
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
index 6866b177c6e..737ad516577 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
@@ -204,7 +204,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$1");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
-        REQUIRE_FALSE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
@@ -218,7 +218,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$2");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
-        REQUIRE_FALSE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
@@ -230,7 +230,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$3");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
-        REQUIRE_FALSE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }
@@ -242,7 +242,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::ContainsAnonymousClass$4");
         const java_class_typet java_class =
           to_java_class_type(class_symbol.type);
-        REQUIRE_FALSE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
       }
     }

From 5350133c8665f7f3f65190f6f51807e6296b3198 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Wed, 4 Jul 2018 15:00:25 +0100
Subject: [PATCH 8/8] Refactor inner class parsing.

---
 jbmc/src/java_bytecode/java_bytecode_parser.cpp | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index a1e749d11e8..53b69181fe2 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1612,19 +1612,16 @@ void java_bytecode_parsert::rinner_classes_attribute(
   for(int i = 0; i < number_of_classes; i++)
   {
     u2 inner_class_info_index = read_u2();
-    UNUSED u2 outer_class_info_index = read_u2();
+    u2 outer_class_info_index = read_u2();
     UNUSED u2 inner_name_index = read_u2();
     u2 inner_class_access_flags = read_u2();
 
-    if(inner_class_info_index == 0)
-      continue;
-
     std::string inner_class_info_name =
       class_infot(pool_entry(inner_class_info_index))
         .get_name(pool_entry_lambda);
-    bool is_private = inner_class_access_flags & ACC_PRIVATE;
-    bool is_public = inner_class_access_flags & ACC_PUBLIC;
-    bool is_protected = inner_class_access_flags & ACC_PROTECTED;
+    bool is_private = (inner_class_access_flags & ACC_PRIVATE) != 0;
+    bool is_public = (inner_class_access_flags & ACC_PUBLIC) != 0;
+    bool is_protected = (inner_class_access_flags & ACC_PROTECTED) != 0;
 
     // If the original parsed class name matches the inner class name,
     // the parsed class is an inner class, so overwrite the parsed class'