From 94c2ccdc3ae5886a27efba02f4e59f26a94f502d Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 23 Jan 2018 10:50:12 +0000
Subject: [PATCH] Regression test for remove_virtual_functions

This test shows that coverage issue with virtual functions is fixed (TG-1404).
---
 .../MyHashMap$EntrySet.class                  | Bin 0 -> 479 bytes
 .../MyHashMap$KeySet.class                    | Bin 0 -> 475 bytes
 .../MyHashMap$UselessIterator.class           | Bin 0 -> 510 bytes
 .../remove-virtual-functions/MyHashMap.class  | Bin 0 -> 1008 bytes
 .../remove-virtual-functions/MyHashMap.java   |  60 ++++++++++++++++++
 .../remove-virtual-functions/MyIterator.class | Bin 0 -> 150 bytes
 .../remove-virtual-functions/MyIterator.java  |   7 ++
 .../remove-virtual-functions/MySet.class      | Bin 0 -> 127 bytes
 .../remove-virtual-functions/MySet.java       |   5 ++
 .../remove-virtual-functions/test.desc        |   8 +++
 10 files changed, 80 insertions(+)
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyHashMap$EntrySet.class
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyHashMap$KeySet.class
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyHashMap$UselessIterator.class
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyHashMap.class
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyHashMap.java
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyIterator.class
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MyIterator.java
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MySet.class
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/MySet.java
 create mode 100644 regression/jbmc-cover/remove-virtual-functions/test.desc

diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap$EntrySet.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$EntrySet.class
new file mode 100644
index 0000000000000000000000000000000000000000..f8dcad30c5688e398ecf6d138cc7a6bec28d1723
GIT binary patch
literal 479
zcmZXR%}&BV6ot>UKxwH^tBCj?!vZi77w$A}h(;371#04Q3KJ=*#dL}ZZ>5QbL=zvt
zhcez#1fz?Yx%ZoU&Yhq4kC!(9``9#*gli#%1p|2tI+hI-4XheiV@Sn4UzYY5GR@ZL
zl*?X=-yIM>^g};BV#t<%@yZoLqCV&fhFsGR#o6%I6VV0t0wQTY77>pJkrGu%)tKaD
zXSD~zs3T5%RhXSN+U@guZX*rThJ|$l8w|ziZs}5rKuG!HLrwn?yAg&Wss~(3A(csn
z!JRoAhjBD&i<nL~3mw(97Vz+<cJB2>hjx>#?<&2lu4qmTutjf|0)qkOIO?GEq#6xs
zMAW8eoANJG-FXJ9j-fpgWtgK`DS<rZkwtD&U!o6C)P9A2U3~%@Bk}M@Q6NW$m`2J1
Qtu9467O_NelGYXA6Ft*jYXATM

literal 0
HcmV?d00001

diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap$KeySet.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$KeySet.class
new file mode 100644
index 0000000000000000000000000000000000000000..4ef4342a6bc85e48efcd4662c4543397657ff3c6
GIT binary patch
literal 475
zcmZXQ%}&BV6ot>UltQUc@fZJNSO6Mu;ZEa*#7LyNKuuf@Fp-j4OsAOeR+?x?H1Pp^
zDB~T4YIHF(_kMHFxik0u<K+#&J~q=ZkhhS;oQVYsI+jfoOstw%V@O6lPZswWGEH}M
z!e!6pcL#(Iy}*l(7_y~bynMxws1Le=A=mT*aW=edi|~TCeIh9@5+RQUp%Rrz)tKaD
zXSD{yup^E=RhW$%Rr~y&+ejg8!@|0W4TeH|TfCIQ7gA1rsOdjqH-bQfb)QQqq%z4c
zI6n@jV$>25eP<dts$<RP!A<SF-4`9YGu-bQy`;XEj>Xubxh271f;o<QB#l#}MNNp>
z6m3)fMJhYbV3jenN1_Zfv@0dBi&<omo75L+_=?)E(61{`U}Gd6{wS*C=n&ILxkP84
OA|3Nsq}ZTy1^5K8?OekE

literal 0
HcmV?d00001

diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap$UselessIterator.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap$UselessIterator.class
new file mode 100644
index 0000000000000000000000000000000000000000..a413e546247133cfefb7c94f310ca8d7496d94cf
GIT binary patch
literal 510
zcmZWl%TB^T6g@)=m9|2~Cn}%@6R3%}aHnx0iID_!;bY-$iW4a*t?3ja|K!F*V&cLN
z@S}{kjj0+JbLY;P^SCn~pKtE~_EF12#iEWZmf~(%Ls`SRh6)37Xx%X6qJb;xdkjXm
zH#y~U(Bt<91RuJ-8yzte8o%)7HG|p?ZUsZJ>-yqsJaR;M$sLanLk1&p90Z==K7-O|
zlDq1Q$0#|FQojhsVPBlMF}ska?GE_^H<5>K!a&J{h8Yc2hH^@&UrFH!DLat}c@%^c
z{|_-czAwVI$E6gK!HQj59{2BB=gv^{X$rkJ`7y|+=GdUG$%5XD4E-9V1C|xfLnnon
z0h4ZLscR7<<`nInDVY6=jIB<gJQGAOqFP7<6%tpeuMt{=^)0T@&WMw>U!Xjtl3W6A
pQk_GIYMir0DKRx?D}U_uB)v}4Zc{f;j0_gAM!QaY6)RW;z5v{vS4{u_

literal 0
HcmV?d00001

diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap.class b/regression/jbmc-cover/remove-virtual-functions/MyHashMap.class
new file mode 100644
index 0000000000000000000000000000000000000000..dea0a5b7d65b80db5012825a76f61c7cc8d263e2
GIT binary patch
literal 1008
zcmZuw?M@R>5IwiM?RK|ITS`U2PXw`D5LCWI5I=~<hE{)6O~5}cc!PzqCA*6e-^3^I
zk3Td42@-t(-^Ld}&s|EJ2x&4i_s%&pbLMV;AO83SU>pxEWZ)PWGGSs^nHvU1EW|Nt
z;HCvb`CAt69c6B(Foy9ICNQbYlz}?}i3Pb`m7#!L@;vF!*WDnHfq`j(%*#O5We}7?
z>APXW7f3$#LjMRJ58dUu6v)3WuetBt(Youcj+VSou1bGKKo4pknH42=n5}uWa85ug
z6kjnj-+0SRrd;#nv#pI~>AyItq-}0-jPAlI^%O5DTfNOfv0PDOuu)>YIlmstfP6Mt
z66mOg?#g<_-Hd8;2?p*OAl#}pw)_?Oq^4$1SGJ$J!8^i6lm;6;=oRQZp~uD<blW(K
za{{>*XW)1liZ?5eZD)>mYPPOyT*eg+VdEa=IEjt>=(q7eHO#gfK3`swD^$_bA`YB*
zgm@&KQYzc+mq{16k*1iLXkE3|tEHoL9b>tKRM6Ovj~b1-bUi+ZCqIPf;|G%AR~6%r
zYNLpP>Eqx$=%qc+(-iZ9zRTHzaI(pti0wjiv|Z@mcr9>&HV2(HNo%457SAbWF5*(N
z$OwzZ6wcWpcX0>$lKzGjhN|rvR)k2SlVb_By(YI08Y93wKzxxyB);-+)HV?%a<qM?
z!3_mZ{tqv5#;fQjNy)3Rt43cqfVsE_Yr*-BRC#D0wm@Zg9~}apU^7SyeE$1K|3Yjm
z(%g##<1wlpr{)RdF-gT!7{oLNn8_e^h`fPo1_ljW?<B1dk&BcF?pNdg)kKzYj=qaN
IPM-(<0mw_Y{{R30

literal 0
HcmV?d00001

diff --git a/regression/jbmc-cover/remove-virtual-functions/MyHashMap.java b/regression/jbmc-cover/remove-virtual-functions/MyHashMap.java
new file mode 100644
index 00000000000..3d69bc6859b
--- /dev/null
+++ b/regression/jbmc-cover/remove-virtual-functions/MyHashMap.java
@@ -0,0 +1,60 @@
+import java.io.PrintStream;
+
+public class MyHashMap {
+
+    private Integer[] table;
+    private int size;
+
+    public MyHashMap() {
+        table = new Integer[8];
+        size = 0;
+    }
+
+    public void put(Integer key) {
+        table[size++] = key;
+    }
+
+    public MySet entrySet() {
+        return new EntrySet();
+    }
+    
+    class EntrySet implements MySet {
+        public final MyIterator iterator() {
+            return new UselessIterator();
+        }
+    }
+
+    class UselessIterator implements MyIterator {
+        boolean b;
+        UselessIterator() {
+            b = true;
+        }
+        public boolean someBoolean() {
+            return b;
+        }
+        public void next() {
+            b = false;
+        }
+    }
+
+    public MySet keySet() {
+        return new KeySet();
+    }
+
+    class KeySet implements MySet {
+        public final MyIterator iterator() {
+            return new UselessIterator();
+        }
+    }
+
+    public static boolean test() {
+        MyHashMap hm = new MyHashMap();
+        MySet es = hm.entrySet();
+        MyIterator it = es.iterator();
+        while (it.someBoolean()) {
+            it.next();
+        }
+        return true;
+    }
+
+}
diff --git a/regression/jbmc-cover/remove-virtual-functions/MyIterator.class b/regression/jbmc-cover/remove-virtual-functions/MyIterator.class
new file mode 100644
index 0000000000000000000000000000000000000000..ed2abe7d5fbf6bd969f904e710a184b4ac256354
GIT binary patch
literal 150
zcmX^0Z`VEs1_l!bZgvJvb_Om+2JYhg+*GIh{G8OpJVpj)4b3P<29~_kiV`p<jFEvW
zIKQ+gIn^yQCzX+b-?!4UB(*59B)>>6E3qsQD2)(dWDo#}>E|TorR)1AWu+#UurV?)
gGB5#cWME)o0h-9b!oUEeSsB=XB8&{|AaMo`00!P4iU0rr

literal 0
HcmV?d00001

diff --git a/regression/jbmc-cover/remove-virtual-functions/MyIterator.java b/regression/jbmc-cover/remove-virtual-functions/MyIterator.java
new file mode 100644
index 00000000000..7b5caca0887
--- /dev/null
+++ b/regression/jbmc-cover/remove-virtual-functions/MyIterator.java
@@ -0,0 +1,7 @@
+public interface MyIterator {
+
+    boolean someBoolean();
+
+    void next();
+
+}
diff --git a/regression/jbmc-cover/remove-virtual-functions/MySet.class b/regression/jbmc-cover/remove-virtual-functions/MySet.class
new file mode 100644
index 0000000000000000000000000000000000000000..a2dc2f43c6dd232edffb8e22632bbe938f605a1f
GIT binary patch
literal 127
zcmX^0Z`VEs1_l!bPId-%b_Nbc29C^<)S|?a{31pMJ`GJD-%3v?-<pwuD>%QjC^^+F
zGba_u@vRI_Ez!$LEK6i$U<Gp+83aIF{hY+SbbbG%tkmQZHbw?U1}2~t3=E7cj10^S
OEFcyGE0APjU;_YEXdCqa

literal 0
HcmV?d00001

diff --git a/regression/jbmc-cover/remove-virtual-functions/MySet.java b/regression/jbmc-cover/remove-virtual-functions/MySet.java
new file mode 100644
index 00000000000..a349d79a305
--- /dev/null
+++ b/regression/jbmc-cover/remove-virtual-functions/MySet.java
@@ -0,0 +1,5 @@
+public interface MySet {
+
+    public MyIterator iterator();
+
+}
diff --git a/regression/jbmc-cover/remove-virtual-functions/test.desc b/regression/jbmc-cover/remove-virtual-functions/test.desc
new file mode 100644
index 00000000000..49ff38dd402
--- /dev/null
+++ b/regression/jbmc-cover/remove-virtual-functions/test.desc
@@ -0,0 +1,8 @@
+CORE
+MyHashMap.class
+--function MyHashMap.test --unwind 5 --cover location
+java::MyHashMap.test.*coverage.*SATISFIED
+--
+java::MyHashMap.test.*coverage.*FAILED
+--
+Checks that TG-1404 is fixed