From 8201c19e997ba7cb5c9bf00963bf6e05bb891548 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Fri, 13 Jul 2018 14:16:08 +0100
Subject: [PATCH 1/2] Parse and capture outer class for inner classes.

---
 jbmc/src/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        |  5 +++++
 jbmc/src/java_bytecode/java_types.h                    | 10 ++++++++++
 src/util/irep_ids.def                                  |  1 +
 5 files changed, 18 insertions(+)

diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index f00a0bfb17c..36ad3bff30d 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -279,6 +279,7 @@ void java_bytecode_convert_classt::convert(
   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);
+  class_type.set_outer_class(c.outer_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 431dd4804f5..29b3bb056a5 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
+++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -221,6 +221,7 @@ class java_bytecode_parse_treet
     bool is_static_class = false;
     bool is_anonymous_class = false;
     bool attribute_bootstrapmethods_read = false;
+    irep_idt outer_class; // when no outer class is set, there is no outer class
     size_t enum_elements=0;
 
     enum class method_handle_typet
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 8bcb491939e..0ac957a849b 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1643,6 +1643,11 @@ void java_bytecode_parsert::rinner_classes_attribute(
     }
     else
     {
+      std::string outer_class_info_name =
+        class_infot(pool_entry(outer_class_info_index))
+          .get_name(pool_entry_lambda);
+      parsed_class.outer_class =
+        constant(outer_class_info_index).type().get(ID_C_base_name);
       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 8e9f092eee6..a82f30a260e 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -121,6 +121,16 @@ class java_class_typet:public class_typet
     return set(ID_is_inner_class, is_inner_class);
   }
 
+  const irep_idt get_outer_class() const
+  {
+    return get(ID_outer_class);
+  }
+
+  void set_outer_class(irep_idt outer_class)
+  {
+    return set(ID_outer_class, outer_class);
+  }
+
   const bool get_is_static_class() const
   {
     return get_bool(ID_is_static);
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index e2d7d160112..bcc6a8f6906 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -675,6 +675,7 @@ IREP_ID_ONE(interface)
 IREP_ID_TWO(C_must_not_throw, #must_not_throw)
 IREP_ID_ONE(is_inner_class)
 IREP_ID_ONE(is_anonymous)
+IREP_ID_ONE(outer_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 c959c3fba81f7a3f2e85fffe643f03361cd60114 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Fri, 13 Jul 2018 15:12:37 +0100
Subject: [PATCH 2/2] Tests get_outer_class with deeply nested classes.

---
 .../ContainsAnonymousClass$1.class            | Bin 491 -> 491 bytes
 .../ContainsAnonymousClass$2.class            | Bin 491 -> 491 bytes
 .../ContainsAnonymousClass$3.class            | Bin 491 -> 491 bytes
 .../ContainsAnonymousClass$4.class            | Bin 491 -> 491 bytes
 .../ContainsAnonymousClass.class              | Bin 761 -> 761 bytes
 .../ContainsLocalClass$1LocalClass.class      | Bin 455 -> 455 bytes
 .../ContainsLocalClass.class                  | Bin 330 -> 330 bytes
 .../java_bytecode_parser/InnerClasses.java    |  66 +++++
 ...eClass$DefaultDoublyNestedInnerClass.class | Bin 0 -> 666 bytes
 ...eClass$PrivateDoublyNestedInnerClass.class | Bin 0 -> 666 bytes
 ...lass$ProtectedDoublyNestedInnerClass.class | Bin 0 -> 670 bytes
 ...teClass$PublicDoublyNestedInnerClass.class | Bin 0 -> 664 bytes
 ...eeplyNested$SinglyNestedPrivateClass.class | Bin 0 -> 1014 bytes
 .../InnerPrivateClassesDeeplyNested.class     | Bin 0 -> 337 bytes
 ...cClass$DefaultDoublyNestedInnerClass.class | Bin 0 -> 691 bytes
 ...cClass$PrivateDoublyNestedInnerClass.class | Bin 0 -> 691 bytes
 ...lass$ProtectedDoublyNestedInnerClass.class | Bin 0 -> 695 bytes
 ...icClass$PublicDoublyNestedInnerClass.class | Bin 0 -> 689 bytes
 ...DeeplyNested$SinglyNestedPublicClass.class | Bin 0 -> 1056 bytes
 ...uterClassMostRestrictiveDeeplyNested.class | Bin 0 -> 347 bytes
 .../parse_java_attributes.cpp                 | 247 +++++++++++++++++-
 21 files changed, 299 insertions(+), 14 deletions(-)
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$DefaultDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PrivateDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$ProtectedDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PublicDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$DefaultDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PrivateDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$ProtectedDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PublicDoublyNestedInnerClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested.class

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class
index dc41102018b2d63f74580d326c27b10a3eaa3146..77a27888382550a13809b752deaee1583c346359 100644
GIT binary patch
delta 17
ZcmaFO{F-^gE=JaQ44e$}C+}y}0RTNu1`+@O

delta 17
YcmaFO{F-^gE=JZE22O_9$@>{~06DV-jsO4v

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class
index 502987e516222e87c14c67a0af7f43c3d73f5434..fc1723fb3e753244ebed143a1c0ed899a427e12a 100644
GIT binary patch
delta 17
ZcmaFO{F-^gE=Jac44e#$Chup|0RTOD1{eSU

delta 17
YcmaFO{F-^gE=JaP22O^A$@>{~06E<SlmGw#

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class
index 80d5d4a52aefce84739e342b4a1d339efb16a99d..15da3d3d9c3e936d1e8db7d127a8c4e16eb8ec3e 100644
GIT binary patch
delta 17
ZcmaFO{F-^gE=JZR44e#0C+}y}0RTOt1|9$a

delta 17
YcmaFO{F-^gE=JZQ22O_L$@>{~06GT+ng9R*

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class
index d215c74a240e7a022305a6c58c951d81ab80bb43..3dea79cbfdaab6ac3cd7d5172d9d464d38cadbf0 100644
GIT binary patch
delta 17
ZcmaFO{F-^gE=Jbn44e!rChup|0RTPC1|$Fg

delta 17
YcmaFO{F-^gE=JZ=22O^w$@>{~06H-Rpa1{>

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class
index eafeaf17b03d479bda2e694ada5f9a3fc7396333..84f32ec5ee3d6077ec109c6dbd652c06fec73314 100644
GIT binary patch
delta 29
lcmey#`jd6TIwrwc3@i-u7z7v=GRQD2VbEY$K6yWr6#$EB2zUSh

delta 29
kcmey#`jd6TIwrvg1{Q`G1_6e61{sDV1`USP$@`hC0D7ngE&u=k

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class
index 2d58f305b14249e0e7e16af233ccffb9c29b817f..c1d636b312ef2c3759be53ec5315a45b30ec5425 100644
GIT binary patch
delta 25
hcmX@ke4Kg1G)CSH44e$>8Tc7CGKes2n!K1%1psAn2QmNv

delta 25
gcmX@ke4Kg1G)CS$22O@t27ZQo1`&pW$%`3P09qLaDgXcg

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class
index 40be03e68ea3488f54c02281c5ac77a4ffb21549..aa5f1a7fcfacf88d54c52b7c0a9b8f563a9c0524 100644
GIT binary patch
delta 19
bcmX@bbc$&M2P5N}$()R8j9VrfFiHUcJf8(s

delta 19
acmX@bbc$&M2P0$FWKKpk#-hmvj8XtNe+1D0

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java
index 7b4792fa26a..3650237d60e 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java
@@ -85,6 +85,72 @@ private PrivateDoublyNestedInnerClass(int i) {
     }
 }
 
+class InnerPrivateClassesDeeplyNested {
+    private class SinglyNestedPrivateClass {
+        int i;
+        SinglyNestedPrivateClass(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 OuterClassMostRestrictiveDeeplyNested {
+    public class SinglyNestedPublicClass {
+        int i;
+        SinglyNestedPublicClass(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;
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$DefaultDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$DefaultDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..5756a620a6bbc4c4e7ef46cc283ab0f20377d74e
GIT binary patch
literal 666
zcmbVKO-lk{5PrswHf`0_zO0lwcrb$`=nxfNlt2&*4DY)->MPqC`yuqRI!Mr=AJC7A
zW)~zcA$XW~o@Zv>`C`6*KED85qnttlyJ;k`7ovR)2O5e5QX*}_mOoKm<x0abq1aQ-
z*naD>=kxH%Rddtlrfqs2L2o+_yAffbx1ETu#<167eqH{q{FmxZO5Q6+`3*v&x_O%R
zd7qGI&W23Lb(F*1;KgG1*|co2q<gc#9q@w+Nq)8W%c(gxb!<b|k->?MEog-PrsGsv
zJTe2@Z_NU0Is0EZLV1nf2-~UKrZcWTT2mhQ8cKwlP1_;FtKni!*CfE1+(J?gBqkyo
z01PACi7*n$AS*g2s4fw4(Ye~i0#y4ztX5he{vHJy@@6CV2q}yOPb54q)))%d5nT|J
M!V%J<6M_zbU*yKOi~s-t

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PrivateDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PrivateDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..992c6e65a73e6729bc34cdb11e13cd9a608b2398
GIT binary patch
literal 666
zcmbVKTT22_5dLPpY}%@;-K>;)@WBj{poggNMF|A4!0>%n2R*W_vAYWWtR5ujp&!tX
zie{H2UqX<>IWynPoVk3=*Z0RKfGd<!h+`*>1a?DhPshHFB7v0LHX#{|m0!8kaYQKg
zlsj@>yX*%%eDu`Z3b^T5zE3dPuFGBoSl~@3!mBatx0qj+zbpTxx|Nc5%2h#w(5P;n
zrhV2Y#GBJ06LKBpa(DJ@v-f1#j#$#Y>C7AOy$V5owfBpOHMb0G!7z})v4JFXLVwe7
zD!&x8rZamv`(HUid5zx;+o?O2JE}j}6CMOQN`&i8+abiNAu%Uw65v#JAt4K*$q@zs
z(+oKg3yCFztjL_8x}ccIT<v@Ts=Y(2l@^G-MS-Tg*~sl71z+?)!t-L)P{6jxf@mom
LA}um5+5xm59s9T9

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$ProtectedDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$ProtectedDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..e491e5e5d3a20018711439684ccd366d7eb3467a
GIT binary patch
literal 670
zcmbVKT}uK%6g{J>o3^>DeOVb2_+SP}&_h)Cq6C7NU_`IGdeM<}Hg;E`pVfl|J@f<m
zQPJH6$(Im(m^t^{Idkuw!+igIegU|~X$Bg0vq)htiuQFJ=qL&Z$*V1p4#zU6T<JI#
zDE6fqxo=$xLK^mbIk!V<x^@r<7;UA<j|nlo?ZkXlLqUt^b$Pq;U#UB8c`ua=8v>2$
z=4IOF&jMQ08<K$8k&3#rsYCvg?YNxD_Pv=upa&U|{OatN6MJqO*n(kT2PX#7&;?#L
zeNLt4dm#<jua-A+maqS7C{SLju%eObuB}G(M`yytbd&^cHXTVIS&hsouPJ~t{tqes
zBnd`#0kEvd7tXM=Y)+2RWL9TIlF_VPEFfwhNYqLTB;RA9#d|J3c9Fr9W5x13XA>x3
Ro3X%A21m#;Y8)Lx`vuX?xp@Ep

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PublicDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PublicDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..f6ebc05850294e31003aa9b22dfe2963f4e5a72d
GIT binary patch
literal 664
zcmbVKT}uK{5Iy79rfs^~mz5EL4`z@AJw$~sN+5^{R?pql!LDp;?5;vTs|N{s=m+$p
zqS>X$mkNBiGjnF<&dfb`-alU70GwbqjRaORNMbFt)(vbJC=y7^X%SMvz4pt;2DS;s
zo_2@MQ-}S42VGB3Rlp5L`98sHxh{JVV1Z}t2+!xR-(-ILzFq#U)VZ|0(5?>ZgnDK1
zGOdGKLZUGqFd^60E_WsmHhb5~cEpqEjVE58FLem=^Rpj~)Kr;Rf@xv}J0?;v2sev9
zr`(;`j_x<dqP~dx=|(919k#+@YL0S;wJUqX{lGwpaJuL)gm@*SW$&K?*q2R6%6h~g
zzX1cVtdJ4$$WjO`S&=zGHOYvJ&Q%X*py~@^)zS>{=P1z<nT^7CNJEKjOL|_sF%+;Y
Qx*%2>TgZq`h_wm&1Q0{EumAu6

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..2cbdcac92768a9ebb94a97c3cbc6bf50bfc803ab
GIT binary patch
literal 1014
zcmbtTO-lk%6g}6ECT&XX(@IlI!wj-Ti=b$u1cI1gMNln9ec6*~jF~a$XSI-^ML(b)
z72O#UTcm<6?z<mz-g#%<z3=P$;}gIUb_4KXBM3h>ohYVYOF@DVtx2P$zgC20i)Pi7
zFPbe1x@K7fwPYB=bQ57IND|_|fMTax@9!Ca6r>1=s@btcgUN=0wwb3W9<;7*4}<Iw
zVpTpuHvUHtNV1g(Gxnpj(uagp*%k8l4}?_|;<>N$gu$oMkoFlNlO2mL?OhXmg-%lt
zLS<=)O82QQ%uB7Vb0t{obj^l1mrfEHT!F9-+S-ezVi8L!mXTHwMnpk|a6Cp|dUzwk
z4rgB1j8^`l-sa0CTu;iD9@#>|%@o8V8$XTak>f(Rnq2e9A@gRPAxMm2N0Q%@pC6fr
zjl0cD*y%rK#I}qT_NyG_8R2Cg%I)_+xp#PSu^zl{E^v+41^4qU0=VP&p5alhdaw?K
ceU1<DA&wcY%yJZ9A7nqrrn1eu3_gTFKb^8L9{>OV

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested.class
new file mode 100644
index 0000000000000000000000000000000000000000..62fe78d71cca8c48827dcc3b423d3280cff929d0
GIT binary patch
literal 337
zcmX^0Z`VEs1_l!bK`sVn23~dsK6VCvb_M}P28rOzy!4z(ztrNA)Rcgt%(BFiROg(;
z;$lVy9?!hI)FLn^706|?$;`_vv14Rl*3b-NWMFa5Pf2BD;P=VQOZ6+wO-d~aNleNC
zif{$zmlh?bx@Cemg2-m*WhIs+@-VP7a4<5+gC&qHOf7avO)Y>qg^@u3q*^~GF)v-;
zKPf9UxrC9yf`BF!T%KW2U|<4z90VAF80Z2Z%?V`50%?#4tJZb~#*JWUE+EMU7K{LD
X;s)}V7<hmp3=CXAQ5GPNm4OKWzZFv`

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$DefaultDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$DefaultDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..3d617927ca062829cd56171cbce0cc0aba431c8e
GIT binary patch
literal 691
zcmbtST}uK%6g}6kO<Q%f5BpH)!N3fXptrsrlt3_zj9z-$)yYP--PoNK`UTa`=|O@X
z`T_l@=&l&`5(Pfox#!Hib7tmn-#=d80PLZZL<|cl#IYEnB@N3ORtO|HnuLV9k$!ns
z!y2K`mCnGvZwp_E{#jtzvRAiF-zVrz#}VFy2&TuaPN1gz)b-UlpYUW)$&qLXarY%r
z{zY$}uRV~CR7Zq*Wk#*$)+HfUcl&~nZAnM8gIh~@7p7(NPO9q$UQe9JkmP>;VrOWM
zOdWI3b)>PbBLR(YHPgq+4RLJ-wraR+-qgqMI|-#f>PGmcnr%9RTE`lSp3+bx9M1G6
zLbMWEwD~U;Z19l8d2%8g><C~Op-0S!BaIB_ETbBCL^)@x+hb7m1(9lTjOg>E(cm>R
fDL){IN5)Uwp5xsJ@|fqGXOzS$QY;r^Q~*8!P$I&P

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PrivateDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PrivateDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..5644211bd9899381ee710d89144f26c81ebfb7c8
GIT binary patch
literal 691
zcmbtS%SyvQ6g`tZVrtr^^-&)!xTsJo7zB5|7A-=dw#AAYS4le5DKU{`Qt&&}4{=ch
z7k+>rCEk>ZZbYFBGxwZ(@0^)A%=^dd8-N2;G$gT<K?=(;T2Zm8VvT_bnk|O3yb)n_
zU&RJPsV}^td*9)q<bz&hyTWO>Rv0qqEzje@lyIV_?QSGz{M--a1?>ogBgL3EIludo
zsQ#jNNXH%tPskI7Mr}^5*3K0}vf&RnL%uCM-idB)9$Z?sOPNgHj{=9EiI^0AzG81=
zjV&Du&~;?7sUr=Q;d-uzReOOLTaq_@GH>SN_n8cpKk7z&C)2gOq1m-Z+>t8E499cb
zi6K#oE!zH<3byEzr0C};G{_OaFk+7=!zhzQj$)peNi0DzU*Da8)nB00%M&D?r;P@!
gxoP<U8XgHhQG0>13W`{ySR|xj9T}2K5-LIY1dA-f<NyEw

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$ProtectedDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$ProtectedDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..594fcb965c46ffce18b8bca0980b3d5adb38021b
GIT binary patch
literal 695
zcmbtS+e*Vg5Ix&lOpQ%iFZEK9LWNqvBKYR*p+zXvwpj7aha_F<mY7JgDfkiUxA;&5
zAN&A6N}Pm>zKB8}c4yA)?3tOvynnpD0XV>>iWC;JNMkATmKCfhSY=>>PKzNUZ$wbp
zSFp}d><f43+;?~&`JfkCj<6e!83YVk%XPUQ15WU?-3{dwpL>D4pdY@lr5N)j=XYNe
zm0$P{sqB$(g*;(sRA=OB?OZXW8s302=xyQhPIzl^|I)M^ie&p<=-d2EL?HijioKCJ
zHZ{ya)3AUI4H+m5*E0=P>G_`IHmTS2NWQ6(-&Gm5{>(6<zUq$Y4(nZOL}Us|497F|
z#gME<GHw5h1!Y>4G;L3UEU5w*Mx+x(NNEx)M^-0Pr;H?7y|z06tGysmD@~AmjuQ>K
gbMf;7R6LUZMCo~oCQ!gU*#dbg){u>9RTPo>1ZbMXdjJ3c

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PublicDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PublicDoublyNestedInnerClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..965e22f81c1217046b795c807a46961b649d7609
GIT binary patch
literal 689
zcmbtSOH0E*5dNmG*c#ikKI)?$gbKBSMeye9&>|FSD^@&sOVXuoiHRhef=Bfic_@Mh
ze}F$qoYab56rqQmoo{ybo7r#Y?fvByz#i7qNMJsLBo-oXQNxmkWdccFO+rdt%b>ig
zVU<wqO1JOawMC#r?<}+&Y1bVy2nc%9b%j3$g5hzi6RHV5^#XOyH+*R;ITQ^cZoeqX
zzwqsI*#qfHbwsFFrsQgFT@n&?uO|q(mUKlsys?CTVOkDHGF>n9ZE+$akpKCLoq;(t
zb<9B5F^4rBDQJYNsUBAT6s_U0b`u%DOA<<d9~)6eHOF-OwT?9qw$e}{98T2{Azq0D
z+WZ#_Hh4smJU21$7eNCIBT|SXJS{9!mTitvjWgoB=c?NyQ1uzHYH5V{(>T#!n;jqD
dBaH|4A2~hG(HIJt<-NdO8Y{>!U4p$L=mTc!!Lk4V

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass.class
new file mode 100644
index 0000000000000000000000000000000000000000..ee361a25684ecdab18ce19f70b740fff156e7e05
GIT binary patch
literal 1056
zcmbtT$xZ@65Pb!sBRC4UFSvsuCgQ=H%LQUW;zHDT(0CZI)h6SNndu=hQUA$<G4bFB
z_)*515#vP&35V*c?tb;Uy8G4V*ZT*6O)STtVJeOuOb1a~$E=Py!uW}_Z>)zy;VE%d
z@vD}s6)n^A2u9hqg&R(Ur(>QlQ*mX(RHEcCu9@-&(y>68tGJF5HRfssT4bJ*xHf%D
zwSp`W(m$pAk06j_D-(Lvt@JV*gq8gxUp1>ea6EO)_i<%S$%ZHiasONG7N=}WTdG~c
zTCT&K^6D8uD>_$#kl2^DIP~wT!aX&s7O%ul9N(>pJsC_=f6pPj^}5+G4Gdw}zz8x1
zl1S;u5_USOHPiBEk^ynSGVPnfQMJymO}OZaGSl{B376fnx79?~)wh)s;k?W0!=`AZ
z#Aq&1N4BFQu)v+y!|fPhV=?fM4CKKxVjICI`!S9RjEJ&N<kwz7`8P!J=~qNwLf|-$
tgW>igVtC^Cnc)+>8o?xV_IW-;!wh<vu8*S_@5I^nvl(myA%lhl=o?>GLVN%K

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested.class
new file mode 100644
index 0000000000000000000000000000000000000000..466827419bf8139ef6a6823a06d2f6cc614abf4f
GIT binary patch
literal 347
zcma)&&uRiO5XQgp-?rOr)sv?}4=rd9dg-zCq6mdni<aKA>mZSsExTF4$LdM&&<F6L
z#Mz~VUJ3>#Gruo<lS%f6-8X;-G<}qD>EX&l-9v-WnrXW*n=z-3=WkhPbTlw3O$ouX
zwVV{dg0)9&wd)hg?al|GGKl9)sK02-<7^dj@~%Q7ia(39B;t|Iq4~E*cd6DYfQK`}
z-6V5A&0pixP38JTM^3MK$o%;`522BJdPdnrZxSv!a)hUothfKX3pXgq7vzg1WEjck
iQe8{VmFoQ#^i>@Dveyc6Bc=<X5&}^GU(||F6?6n-nOBGa

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
index c823c1acae5..367e343acb8 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
@@ -22,7 +22,7 @@ SCENARIO(
       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")
+      THEN("The inner class should be marked as public")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass");
@@ -31,11 +31,12 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_public);
+        REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses");
       }
     }
     WHEN("Parsing the InnerClasses attribute for a package private inner class")
     {
-      THEN("The class should be marked as default")
+      THEN("The inner class should be marked as default")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass");
@@ -44,11 +45,12 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_default);
+        REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses");
       }
     }
     WHEN("Parsing the InnerClasses attribute for a protected inner class")
     {
-      THEN("The class should be marked as protected")
+      THEN("The inner class should be marked as protected")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass");
@@ -57,11 +59,12 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_protected);
+        REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses");
       }
     }
     WHEN("Parsing the InnerClasses attribute for a private inner class")
     {
-      THEN("The class should be marked as private")
+      THEN("The inner class should be marked as private")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass");
@@ -70,10 +73,13 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses");
       }
     }
   }
-  GIVEN("Some package-private class files in the class path with inner classes")
+  GIVEN(
+    "Some package-private (default) class files in the class path with inner "
+    "classes")
   {
     const symbol_tablet &new_symbol_table = load_java_class(
       "InnerClassesDefault", "./java_bytecode/java_bytecode_parser");
@@ -88,11 +94,15 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_public);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) == "InnerClassesDefault");
       }
     }
-    WHEN("Parsing the InnerClasses attribute for a package private inner class")
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private (default) "
+      "inner class")
     {
-      THEN("The class should be marked as default")
+      THEN("The inner class should be marked as package-private (default)")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDefault$DefaultInnerClass");
@@ -101,6 +111,8 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_default);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) == "InnerClassesDefault");
       }
     }
     WHEN("Parsing the InnerClasses attribute for a protected inner class")
@@ -114,11 +126,13 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_protected);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) == "InnerClassesDefault");
       }
     }
     WHEN("Parsing the InnerClasses attribute for a private inner class")
     {
-      THEN("The class should be marked as private")
+      THEN("The inner class should be marked as private")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDefault$PrivateInnerClass");
@@ -127,6 +141,8 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) == "InnerClassesDefault");
       }
     }
   }
@@ -151,54 +167,246 @@ SCENARIO(
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_public);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerClassesDeeplyNested$SinglyNestedClass");
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private (default) "
+      "doubly-nested inner class")
+    {
+      THEN("The inner class should be marked as package-private (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_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerClassesDeeplyNested$SinglyNestedClass");
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private (default) "
+      "doubly-nested inner class ")
+    {
+      THEN("The inner 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_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_protected);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerClassesDeeplyNested$SinglyNestedClass");
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a private doubly-nested inner "
+      "class")
+    {
+      THEN("The inner 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_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerClassesDeeplyNested$SinglyNestedClass");
+      }
+    }
+  }
+
+  GIVEN(
+    "Some package-private class files in the class path with private deeply"
+    "nested inner classes")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "InnerPrivateClassesDeeplyNested",
+      "./java_bytecode/java_bytecode_parser");
+    WHEN(
+      "Parsing the InnerClasses attribute for a public doubly-nested inner "
+      "class")
+    {
+      THEN(
+        "The inner class should be marked as private because its containing "
+        "class has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
+          "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass");
       }
     }
     WHEN(
       "Parsing the InnerClasses attribute for a package private doubly-nested "
       "inner class")
     {
-      THEN("The class should be marked as default")
+      THEN(
+        "The inner class should be marked as private because its containing "
+        "class has stricter access ")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
-          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
           "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass");
       }
     }
     WHEN(
       "Parsing the InnerClasses attribute for a protected doubly-nested inner "
       "class")
     {
-      THEN("The class should be marked as protected")
+      THEN(
+        "The inner class should be marked as private because its containing "
+        "class has stricter access ")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
-          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
           "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass");
       }
     }
     WHEN(
       "Parsing the InnerClasses attribute for a private doubly-nested inner "
       "class")
     {
-      THEN("The class should be marked as private")
+      THEN("The inner class should be marked as private ")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
-          "java::InnerClassesDeeplyNested$SinglyNestedClass$"
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
+          "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass");
+      }
+    }
+  }
+
+  GIVEN(
+    "Some class files where the outer class is more restrictive than the first "
+    "inner class")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "OuterClassMostRestrictiveDeeplyNested",
+      "./java_bytecode/java_bytecode_parser");
+    WHEN(
+      "Parsing the InnerClasses attribute for a public doubly-nested inner "
+      "class")
+    {
+      THEN(
+        "The inner class should be marked as default (package-private) because "
+        "one of its containing classes has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass");
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private doubly-nested "
+      "inner class")
+    {
+      THEN(
+        "The inner class should be marked as default (package-private) because "
+        "one of its containing classes has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass");
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a protected doubly-nested inner "
+      "class")
+    {
+      THEN("The inner class should be marked as default (package-private)")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass");
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a private doubly-nested inner "
+      "class")
+    {
+      THEN("The inner class should be marked as private")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
           "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);
+        REQUIRE(
+          id2string(java_class.get_outer_class()) ==
+          "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass");
       }
     }
   }
@@ -219,6 +427,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
     WHEN(
@@ -234,6 +443,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
     WHEN("Parsing the InnerClasses attribute for a protected anonymous class")
@@ -247,6 +457,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
     WHEN("Parsing the InnerClasses attribute for a private anonymous class")
@@ -260,6 +471,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_access() == ID_private);
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
   }
@@ -280,6 +492,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_access() == ID_private);
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
   }
@@ -299,6 +512,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_static_class());
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(id2string(java_class.get_outer_class()) == "StaticInnerClass");
       }
     }
     WHEN("Parsing the InnerClasses attribute for a non-static inner class ")
@@ -312,6 +526,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(id2string(java_class.get_outer_class()) == "StaticInnerClass");
       }
     }
   }
@@ -328,6 +543,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE(java_class.get_is_static_class());
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
     WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ")
@@ -341,6 +557,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE(java_class.get_is_anonymous_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
   }
@@ -359,6 +576,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
     WHEN(
@@ -374,6 +592,7 @@ SCENARIO(
         REQUIRE(java_class.get_is_inner_class());
         REQUIRE_FALSE(java_class.get_is_static_class());
         REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_outer_class().empty());
       }
     }
   }