From b1efed4d8648e35d5506f81ca13abb1f8f9a9252 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 1 Feb 2019 16:35:23 +0000
Subject: [PATCH] Add test for accessing a qualified generic member field

---
 .../jbmc/return-generic-member/Generic.class      | Bin 0 -> 366 bytes
 .../jbmc/return-generic-member/Test.class         | Bin 0 -> 453 bytes
 .../jbmc/return-generic-member/Test.java          |  11 +++++++++++
 .../jbmc/return-generic-member/test.desc          |  13 +++++++++++++
 4 files changed, 24 insertions(+)
 create mode 100644 jbmc/regression/jbmc/return-generic-member/Generic.class
 create mode 100644 jbmc/regression/jbmc/return-generic-member/Test.class
 create mode 100644 jbmc/regression/jbmc/return-generic-member/Test.java
 create mode 100644 jbmc/regression/jbmc/return-generic-member/test.desc

diff --git a/jbmc/regression/jbmc/return-generic-member/Generic.class b/jbmc/regression/jbmc/return-generic-member/Generic.class
new file mode 100644
index 0000000000000000000000000000000000000000..5b4aa70ef4e418dfca88a92a5cb49fedc60ef763
GIT binary patch
literal 366
zcmZXPF;BxV5QX10X+qM_mV%fW3j<x4NE8Vn!4knxtGg4d;wm`EO_2CmOh^p;0DctW
z6563)$@kuUdOn@MzCS(zT;M2#g99HEABO}l(MH!P!I_>e2<~<Dpa`Q(8+F$_<;n_~
zmrN#ERmgH7t#11bbn8dGCIs27GRo>ACLHhPUZ1zw;Wm^A5vQCC=6Y#l-B_MJO~hrk
zk}q;rO0%5Z=POmzarz$-!g<x$Lfz<gt3arAecnEd;G$3PH=7W~f5+hjJ^p!nh%d)k
rJ$6^DE$N@VgWlLU@VR;&9AJ-q^cz5ckh{SSiMZ=wzpF!xIvxK2vVKgj

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/return-generic-member/Test.class b/jbmc/regression/jbmc/return-generic-member/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..eee121128792d314fbbcfb6867bc80d3045d18eb
GIT binary patch
literal 453
zcmZ`#O;5r=6r3$BwWSK;_r>T9IM|Cf2p1ELNuvh{_ob}3q%27({w_^SOg#7l{87eP
zkPs8iX5ZU4J2UU?etx}w0Jy|S2p0zdN;vd!<l|Vtd(bKy2?WWFGAh?;o9CV$8(A!J
zC2+dNJIO>o$vBf{9N(HkjaA<6l3ea+ql>OUsnHw=xL30gWz|F*b+?!fRo<7wj7UA1
zr7|1HT-*8wbc;tlr$^FP^MYpXRB9toX*Abu37&1L|Aq*Avqhe&Yi&CP*6hMg8zDd#
z!9$tW78R&%UU5I1sI<U2zr*GC2re=ieO3;(xM_xvu|gzf7R+Aj4dP`<i5RWGinke~
j6#+Y_F0mSRY4ThA3g?-Z4#{hA`491GhB^)RmhAm+8_`l4

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/return-generic-member/Test.java b/jbmc/regression/jbmc/return-generic-member/Test.java
new file mode 100644
index 00000000000..dfb8ff26593
--- /dev/null
+++ b/jbmc/regression/jbmc/return-generic-member/Test.java
@@ -0,0 +1,11 @@
+public class Test {
+
+  public Generic<Integer> field;
+
+  public Generic<Integer> main() {
+    return field;
+  }
+
+}
+
+class Generic<T> { }
diff --git a/jbmc/regression/jbmc/return-generic-member/test.desc b/jbmc/regression/jbmc/return-generic-member/test.desc
new file mode 100644
index 00000000000..3b2d8745bdb
--- /dev/null
+++ b/jbmc/regression/jbmc/return-generic-member/test.desc
@@ -0,0 +1,13 @@
+CORE
+Test.class
+--function Test.main --validate-goto-model
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test ensures that the member_exprt generated to return a qualified generic
+field has the correct type, otherwise we'll fail model validation.
+Prior to ec4160829cc9c22ff71e647dd2894439720ad89c we would have created a
+non-matching type (Generic<Integer> vs. Generic)