From c7d8ea647c1c7ed29d3f7e4fa73e82c37a9e8749 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 17 Nov 2017 00:38:57 +0000
Subject: [PATCH] Tests for simplifying ID_string equalities

---
 regression/cbmc-java/virtual8/A.class    | Bin 0 -> 222 bytes
 regression/cbmc-java/virtual8/B.class    | Bin 0 -> 207 bytes
 regression/cbmc-java/virtual8/C.class    | Bin 0 -> 207 bytes
 regression/cbmc-java/virtual8/D.class    | Bin 0 -> 164 bytes
 regression/cbmc-java/virtual8/E.class    | Bin 0 -> 164 bytes
 regression/cbmc-java/virtual8/Test.class | Bin 0 -> 354 bytes
 regression/cbmc-java/virtual8/Test.java  |  29 ++++++++++++++++++++
 regression/cbmc-java/virtual8/test.desc  |  11 ++++++++
 regression/cbmc-java/virtual9/A.class    | Bin 0 -> 222 bytes
 regression/cbmc-java/virtual9/B.class    | Bin 0 -> 207 bytes
 regression/cbmc-java/virtual9/C.class    | Bin 0 -> 207 bytes
 regression/cbmc-java/virtual9/D.class    | Bin 0 -> 164 bytes
 regression/cbmc-java/virtual9/E.class    | Bin 0 -> 164 bytes
 regression/cbmc-java/virtual9/Test.class | Bin 0 -> 456 bytes
 regression/cbmc-java/virtual9/Test.java  |  33 +++++++++++++++++++++++
 regression/cbmc-java/virtual9/test.desc  |  13 +++++++++
 16 files changed, 86 insertions(+)
 create mode 100644 regression/cbmc-java/virtual8/A.class
 create mode 100644 regression/cbmc-java/virtual8/B.class
 create mode 100644 regression/cbmc-java/virtual8/C.class
 create mode 100644 regression/cbmc-java/virtual8/D.class
 create mode 100644 regression/cbmc-java/virtual8/E.class
 create mode 100644 regression/cbmc-java/virtual8/Test.class
 create mode 100644 regression/cbmc-java/virtual8/Test.java
 create mode 100644 regression/cbmc-java/virtual8/test.desc
 create mode 100644 regression/cbmc-java/virtual9/A.class
 create mode 100644 regression/cbmc-java/virtual9/B.class
 create mode 100644 regression/cbmc-java/virtual9/C.class
 create mode 100644 regression/cbmc-java/virtual9/D.class
 create mode 100644 regression/cbmc-java/virtual9/E.class
 create mode 100644 regression/cbmc-java/virtual9/Test.class
 create mode 100644 regression/cbmc-java/virtual9/Test.java
 create mode 100644 regression/cbmc-java/virtual9/test.desc

diff --git a/regression/cbmc-java/virtual8/A.class b/regression/cbmc-java/virtual8/A.class
new file mode 100644
index 0000000000000000000000000000000000000000..680ceb8db5c63d43c9afdd4e7e415ccfaa5ba982
GIT binary patch
literal 222
zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2xA%}16Oc<X;E^jTP8?=GbFXRL@z6`ERlzSg@F~Q!jX|d0L0hN
zNz6;v_fN`7O)g<jU|<4T2Len$3{=Pfv=hjZ1=5T_npJB%1LH;@gOPz9NV0(id4Mbq
WxKc^5EKmiyGG3r!PM{<c0~Y{HP9J6f

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual8/B.class b/regression/cbmc-java/virtual8/B.class
new file mode 100644
index 0000000000000000000000000000000000000000..06e08d314d81d79375fefc3dea075bf1d6ac2e3d
GIT binary patch
literal 207
zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2xA%}16Oc<X;E^jTP8?=GbFXRL@z6`ERlzSg@F~Q!U>2S859_p
zfaZe$6A%Ms7=V@lS+YQy5lFLYZD(NI2xKraumedpu%IB2#Q|3;36=$_KvyONRLlvK
IWMbd~0CT4qssI20

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual8/C.class b/regression/cbmc-java/virtual8/C.class
new file mode 100644
index 0000000000000000000000000000000000000000..6391b1ca05c4835b79cb53ba5edb24acb3fba99d
GIT binary patch
literal 207
zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2xA%}16Oc<X;E^jTP8?=GbFXRL@z6`ERlzSg@F~Q!WoDi859_p
zfaZe$6A%Ms7=V@lS+YQy5lFLYZD(NI2xKraumedpu%IZA#Q|3;36=$_KvyOPRLlvK
IWMbd~0Cfl%vj6}9

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual8/D.class b/regression/cbmc-java/virtual8/D.class
new file mode 100644
index 0000000000000000000000000000000000000000..9cbaf50b562e4cb9d8a1555bf85066d127d80b30
GIT binary patch
literal 164
zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz~}<R&I}3+OhB_i
ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{{<2_!jyJSGNC05!H4MgRZ+

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual8/E.class b/regression/cbmc-java/virtual8/E.class
new file mode 100644
index 0000000000000000000000000000000000000000..fcc8898043c61674bcd559159dbd73c987ff5e9d
GIT binary patch
literal 164
zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz~~CZP7DeROhB_i
ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{{<10*?sJSGNC05#hfNdN!<

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual8/Test.class b/regression/cbmc-java/virtual8/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..f90d0ac64b8cfb7dde24b4a84087a8e75f353d93
GIT binary patch
literal 354
zcmYL@OH0E*6ot=C(o8c>AHE;pqPtqqZrmwCQM$3{!Xmg#>L@8~3Tfm2a$`loAK;G?
z&qS~cb6@k_Gw1u~;|stk4m1?jH8!xRu%+R<Cd9VFj>4`WJWsQ9aUt;ANB4r@a`tEi
zjX|2(n_`;Sd>AJaPJ+D1`o!CV-dPDw<1`cKyIGNsY(I5OG_>=@$vA$A4XTI~_6+tB
z3FOMaphgu(2%3)RPU7sjdz*~yh$HFoKA}Z#ipD{s;zSrVyF+GSu5^}=R~CXb#;_dn
zXD83vp)KY=^bOt$)$sV}BjAZp|5rZd+~KuP_zz12*PVA%R%>;xfR?H}rd(>U_t5+W
D6_PB|

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual8/Test.java b/regression/cbmc-java/virtual8/Test.java
new file mode 100644
index 00000000000..7d5e5b08396
--- /dev/null
+++ b/regression/cbmc-java/virtual8/Test.java
@@ -0,0 +1,29 @@
+public class Test {
+  public static void runF(A x) {
+    x.f();
+  }
+
+  public static void main() {
+    A y = new D();
+    runF(y);
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}
diff --git a/regression/cbmc-java/virtual8/test.desc b/regression/cbmc-java/virtual8/test.desc
new file mode 100644
index 00000000000..774005ac03d
--- /dev/null
+++ b/regression/cbmc-java/virtual8/test.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+C\.f
+--
+A\.f
+B\.f
+D\.f
+E\.f
diff --git a/regression/cbmc-java/virtual9/A.class b/regression/cbmc-java/virtual9/A.class
new file mode 100644
index 0000000000000000000000000000000000000000..145301d5c90c1d24d74e775db4de337459e9813e
GIT binary patch
literal 222
zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2xA%}16Oc<X;E^jTP8?=GbFXRL@z6`ERlzSg@F~Q!jX|d0L0hN
zNz6;v_fN`7O)g<jU|<4T2Len$3{=Pfv=hjZ1=5T_npJB%1LH;@gOPz9NV0(i1%NCL
WxKc^5EKmiyGC`nXPM{<c0~Y{ILLY7b

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual9/B.class b/regression/cbmc-java/virtual9/B.class
new file mode 100644
index 0000000000000000000000000000000000000000..0b628d311bbb5b48f4764c2c190b4c625ce6c1f8
GIT binary patch
literal 207
zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2xA%}16Oc<X;E^jTP8?=GbFXRL@z6`ERlzSg@F~Q!U>2S859_p
zfaZe$6A%Ms7=V@lS+YQy5lFLYZD(NI2xKraumedpu%IZA#Q|3;36=$_KvyOPRLlvK
IWMbd~0CbxfvH$=8

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual9/C.class b/regression/cbmc-java/virtual9/C.class
new file mode 100644
index 0000000000000000000000000000000000000000..abbca958c2d485ab777a0d38a2d6e43f2f2062bc
GIT binary patch
literal 207
zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2xA%}16Oc<X;E^jTP8?=GbFXRL@z6`ERlzSg@F~Q!WoDi859_p
zfaZe$6A%Ms7=V@lS+YQy5lFLYZD(NI2xKraumedpu%IN6#Q|3e;(?T6D3byTa{?up
G7`Om+{299d

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual9/D.class b/regression/cbmc-java/virtual9/D.class
new file mode 100644
index 0000000000000000000000000000000000000000..31b40172c7a4a59ed254b0b6e3546f1b721f8be3
GIT binary patch
literal 164
zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz~}<R&I}3+OhB_i
nfDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{{flH>sLm>4(#HR2db

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual9/E.class b/regression/cbmc-java/virtual9/E.class
new file mode 100644
index 0000000000000000000000000000000000000000..90b2361dc032366210e451a283eb09c614dfa36f
GIT binary patch
literal 164
zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz~~CZP7DeROhB_i
ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{}V03<npJSGNC05%60O#lD@

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual9/Test.class b/regression/cbmc-java/virtual9/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..eec3a1b0d3ee6e93917956aa55265f9e6941687c
GIT binary patch
literal 456
zcmYLE%TB^j5IxhDUi#pnC@P4+u3{n^cN!ByWL0$mF)^$PR#JpwYVmvAxppH)5<b9h
zGRC>pgxtr>J?G4vJ6}JaD*z{`nJ`c^v4dTKJrgR50wohE38qmN*cYe}^s^ug;&X!P
z9NrML_Uz6l<lG?iujbQ%AN9P!gb^*8haHwXZtFA=PQ4%`6rH|1_MW}w#0y8wZX5;S
zDB&~R*c(1vdXGuHzyZPR&gRk3?*y`+(et0;V_9m$gvA0IRagXS^SQ8*MUGviijZGh
zTo1<nkRfXExksI6F?e9`fb0N^Z<}8gj>Iw5Sb*L*A!PX06Oi3yd(Ne_&hbzB4rMJh
zp)jdJ<7FU^jemKcamm!kZLIVcWS3BH7tq{SSWBch)!m~H2-!(VOiOGF2!5rL-xm0n
WWwx#|yUC0J<r@VdH(@I&+x`V3L_viB

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/virtual9/Test.java b/regression/cbmc-java/virtual9/Test.java
new file mode 100644
index 00000000000..024d080275b
--- /dev/null
+++ b/regression/cbmc-java/virtual9/Test.java
@@ -0,0 +1,33 @@
+public class Test {
+  public static void runF(A x) {
+    x.f();
+  }
+
+  public static void main(String[] args) {
+    A y = null;
+    if(args.length==3)
+      y = new C();
+    else
+      y = new E();
+    runF(y);
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}
diff --git a/regression/cbmc-java/virtual9/test.desc b/regression/cbmc-java/virtual9/test.desc
new file mode 100644
index 00000000000..5ec4ac65fd9
--- /dev/null
+++ b/regression/cbmc-java/virtual9/test.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+Test.class
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+B\.f
+C\.f
+--
+A\.f
+D\.f
+E\.f
+--
+could be pruned by a value set analysis