From 320788ce6136edde558e740b4d8e57a6f96a4b28 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 8 Apr 2018 21:33:11 +0100
Subject: [PATCH] Reduce redundancy between jbmc-string and strings-smoke-tests

Several tests are the same or test the same functionality.
---
 .../jbmc-strings/java_append_object/test.desc |   2 +
 .../cprover/CProverString.class               | Bin 4153 -> 0 bytes
 .../cprover/CProverString.java                | 150 ------------------
 .../java_append_int/test.desc                 |   8 -
 .../java_append_int/test_append_int.class     | Bin 842 -> 0 bytes
 .../java_append_int/test_append_int.java      |  11 --
 .../java_append_object/test.desc              |  10 --
 .../test_append_object.class                  | Bin 992 -> 0 bytes
 .../test_append_object.java                   |  17 --
 9 files changed, 2 insertions(+), 196 deletions(-)
 delete mode 100644 regression/strings-smoke-tests/cprover/CProverString.class
 delete mode 100644 regression/strings-smoke-tests/cprover/CProverString.java
 delete mode 100644 regression/strings-smoke-tests/java_append_int/test.desc
 delete mode 100644 regression/strings-smoke-tests/java_append_int/test_append_int.class
 delete mode 100644 regression/strings-smoke-tests/java_append_int/test_append_int.java
 delete mode 100644 regression/strings-smoke-tests/java_append_object/test.desc
 delete mode 100644 regression/strings-smoke-tests/java_append_object/test_append_object.class
 delete mode 100644 regression/strings-smoke-tests/java_append_object/test_append_object.java

diff --git a/regression/jbmc-strings/java_append_object/test.desc b/regression/jbmc-strings/java_append_object/test.desc
index 2af06f2686a..ce08e3e17ad 100644
--- a/regression/jbmc-strings/java_append_object/test.desc
+++ b/regression/jbmc-strings/java_append_object/test.desc
@@ -5,3 +5,5 @@ test_append_object.class
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 15.* FAILURE$
 --
+--
+Issue: diffblue/test-gen#82
diff --git a/regression/strings-smoke-tests/cprover/CProverString.class b/regression/strings-smoke-tests/cprover/CProverString.class
deleted file mode 100644
index 8eb78d4aaa4179eb951b284df7cf07f2b598d2f5..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 4153
zcmbVOTXz#x6#k}3lQtdN(%M!?dJ$04KwGd-Dy<+*DF#ca77<a@G@X=`l9XIP#0y^V
zf){ixAN2u!<)OYrmk<5`f0WB_Po|UP<Rq}#uJz4i_V?|5_C9-`nScNL`yT*D@KXSL
z@oE6CVM*YE!0Q4R1>O+2B=BYnF3a_;0QTT*xw{g;J9t;%J%PBuvOq#$MZgkB3akoT
z4IqUz0ftH8n!viibpiTIAuW&**bulOko6<yN8W&MI+af4PZ;oohc6oNMl&mxfsXl9
z+FB@FU$(Lr;>+uN;!9kOXHQYk8=hZ_-;9r~$J480OZjXny*d>ejvCmpl#eH_or`Zc
zinat@EoM^be0^Drp<LRGmCR%rs@;7O%@ooM*{2H`8>YA`lT7BU{LF1xwjC>Hpe<Ke
zUb1c!taO6jM)l%~B%;i0i$7(cmGYdOmx28{@o<IKDS&~njv3QZeesPAE4^Z1p;j|f
zNUg6}*{O;URm+QMTyAN&Nh{X6m1oiu^*uNCV3s^cOxd-g4gA#RR<V#&I%j3+;7kJt
z6*)R(Y~-?0N|(1QjBZzWcDus4?Fwfb30pY?^HzE_f7L)pSMp?%O%;;~Z)D~ai>IyK
z@2~GEDz1*yw`<$fUW9@1`Z8UPj!HAfGlf!GnqZvc)AhqVS?4){8)T{NyT{A4UH5pI
zw&xsKU@23`Cak%XoYh^?#cbxLl`T!xs2tZO_TgDS3MOvimWeRlH*o;BO^gVP;sX<h
z1P<el0hk!ahXO|hKJw#Z6BGEv#3b&TIF3(EOye_w&jr2^pkW&K1ilpb%8##2MDdM@
zIoucJx1#(`Y~Ks~An-tdhH3n0U{@x)I+ob5mp)dNf`QKRJLmlJnw8+uQt_yiD9^uj
zX9oB(<J-X-wqHzg;jiW}k3L>Qa;@lqs`J%A57`w~_kizJWUisFytL9Y=NME@&#Exh
zE2xsObNjWS%BL$cs9j>&JQ|MGCeTR0c-l@by^8GhXj`_zuI<eVd&6Uo@f)6Qy|opV
zwl8fk&mr!teIBVhyH!_bMuPgXIo6RUt(wDUFm2JwW^K*NW^KuAGpBG5zaZsr0ESF1
z@j3qL=au7$=E$Eg{@@M2P>4SJp$Dy;>tWst^#q#u5A=9~zhh@GQbf~lXpIDm@I3N7
zqM^x_w!_2wX6&GoZnPl6Umh6U^mPCS9bW^EFQ3T0BCd>Uk~^a3HmlrDaz`=d_#I>@
z3Ga^tLq+&hau3Oe>X7{^c{j<2@x0b^%cipAL6XP$p<XIg%t@~=_$w>BY1ir@d|j=Z
zl5ar7rDFB6P~gURxg|bsN;@mPlQoy3dC}wx*lv$HZc}_F*^LH&K_KD@{e`y8knF=l
zbVNLI<6V(w!O&JP7Qrk>8-SncgY+_jHdd{hr5I#E_A$@>%v7Q_!_(I7XV?iGbHWZ$
z;H9Z0av;=S#11w0V`NX_1#O|)Rq_<c$1&xQtNNfr<(?#W8ZXv5K3GJjN}jdJCu+&8
z!A_MNv&kp5<Sv!GV3YOvb*tnhoBWdNxl}s#<4_S#spLyG`IJj`n|EIkJu3N%O`dVd
zuIF$Oy()Q`<S1qx@}A0Z>no3WfX{&>H+_}-Fit!Cs%?2%9gH<{=Wxd1?yVZRU8?gm
z`#M9xBwlt`?xxAD*{!ZTNAhvRbSnv}+*{<1<E++kNG0DPc^a?OlG#oDD*3KWp06cy
t$pb3+o=rZdB@e3P`!-o$j3Jf$z$P!ap4~lXH$9`0e<tlb_p=F${{vOJpdA1J

diff --git a/regression/strings-smoke-tests/cprover/CProverString.java b/regression/strings-smoke-tests/cprover/CProverString.java
deleted file mode 100644
index 0603aac5dc6..00000000000
--- a/regression/strings-smoke-tests/cprover/CProverString.java
+++ /dev/null
@@ -1,150 +0,0 @@
-package org.cprover;
-
-public final class CProverString {
-    public static char charAt(String s, int i) {
-        if (0 <= i && i < s.length())
-            return s.charAt(i);
-        else
-            return '\u0000';
-    }
-
-    public static int codePointAt(String s, int index) {
-        return s.codePointAt(index);
-    }
-
-    public static int codePointBefore(String s, int index) {
-        return s.codePointBefore(index);
-    }
-
-    public static int codePointCount(
-            String s, int beginIndex, int endIndex) {
-        return s.codePointCount(beginIndex, endIndex);
-    }
-
-    public static int offsetByCodePoints(
-            String s, int index, int codePointOffset) {
-        return s.offsetByCodePoints(index, codePointOffset);
-    }
-
-    public static CharSequence subSequence(
-            String s, int beginIndex, int endIndex) {
-        return s.subSequence(beginIndex, endIndex);
-    }
-
-    public static String substring(String s, int i) {
-        if (i <= 0)
-            return s;
-        else if (i >= s.length())
-            return "";
-        else
-            return s.substring(i);
-    }
-
-    public static String substring(String s, int i, int j) {
-        if (i < 0)
-            return substring(s, 0, j);
-        if (j >= s.length())
-            return substring(s, 0, s.length() - 1);
-        if (i >= j)
-            return "";
-        return s.substring(i, j);
-    }
-
-    public static StringBuilder append(
-            StringBuilder sb, CharSequence cs, int i, int j) {
-        return sb.append(cs, i, j);
-    }
-
-    public static StringBuilder delete(StringBuilder sb, int start, int end) {
-        return sb.delete(start, end);
-    }
-
-    public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
-        return sb.deleteCharAt(index);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, String str) {
-        return sb.insert(offset, str);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, boolean b) {
-        return sb.insert(offset, b);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, char c) {
-        return sb.insert(offset, c);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, int i) {
-        return sb.insert(offset, i);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, long l) {
-        return sb.insert(offset, l);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, float f) {
-        return sb.insert(offset, f);
-    }
-
-    public static StringBuilder insert(
-            StringBuilder sb, int offset, double d) {
-        return sb.insert(offset, d);
-    }
-
-    public static void setLength(StringBuffer sb, int newLength) {
-        sb.setLength(newLength);
-    }
-
-    public static char charAt(StringBuffer sb, int index) {
-        return sb.charAt(index);
-    }
-
-    public static void setCharAt(StringBuffer sb, int index, char c) {
-        sb.setCharAt(index, c);
-    }
-
-    public static StringBuffer delete(
-            StringBuffer sb, int start, int end) {
-        return sb.delete(start, end);
-    }
-
-    public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
-        return sb.deleteCharAt(index);
-    }
-
-    public static String substring(StringBuffer sb, int start, int end) {
-        return sb.substring(start, end);
-    }
-
-    public static StringBuffer insert(
-            StringBuffer sb, int offset, String str) {
-        return sb.insert(offset, str);
-    }
-
-    public static StringBuffer insert(
-            StringBuffer sb, int offset, boolean b) {
-        return sb.insert(offset, b);
-    }
-
-    public static StringBuffer insert(
-            StringBuffer sb, int offset, char c) {
-        return sb.insert(offset, c);
-    }
-
-    public static StringBuffer insert(
-            StringBuffer sb, int offset, int i) {
-        return sb.insert(offset, i);
-    }
-
-    public static StringBuffer insert(
-            StringBuffer sb, int offset, long l) {
-        return sb.insert(offset, l);
-    }
-}
diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc
deleted file mode 100644
index 71e874d2486..00000000000
--- a/regression/strings-smoke-tests/java_append_int/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-FUTURE
-test_append_int.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/regression/strings-smoke-tests/java_append_int/test_append_int.class b/regression/strings-smoke-tests/java_append_int/test_append_int.class
deleted file mode 100644
index 16948397e03dc279cdae32b41c8692bcfbb44978..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 842
zcmaJ<O>fgc5Pjo(*l`@3rfC~W0~87*DQ!pza7cxK0upKphaf6?shoIKxwv+)9ezyy
z0B1l-B`U$4{{&*zX&Rssmzmx9c<=4Z{`mFv8-OMr=rB=Maao6gvW6?tUzKKAnrj*4
za9zWSjvKhC;+BrAEU)OOqNZY%FuP)fp$H<!_rj-6Xmwp-6KIc+-gG=CdPqoAs&5F%
zE#DRdv+a1|<>06*g4eQ`6GxWg5ptc#>b={s`f->gsklwhHhb<VjNb7FK~Fq)WK%H`
zVYF}c`@*yL9WPoxv_4n{3YaA<$aCGbyn}it3LNj?$-r@K5wI-Vz#7)2sT;V1hJie0
z2#VcgHUk^DODIj-A5Wh4EC_t=H~(Q((KK)m_X+uF)2r^G=tX~p#xi&$W5I;AN_*Nc
z&bF%OLZ`Z0gr&-h|E0CapHLJl=L;DiE#40-Hzdsc$vl?Ys`9qXsh%yDS4x<-Md$>=
zJ{tlrC>n5r_qm5<{uw6!A<CEJ4EdA*$@#M_@~zCC*r#g8pii<8b8ORbkdVRrS*g!I
zP2t?e36!_TNNm>%$q`b!HFbpaZfyj${TbR2#nnP)1bv9?39?*he3!UNjJwFlOa_g;
z36*0S7MZ019SfYvf_|c*qNL(toSNut#)5#ELT-c$L#WA*NG85On_^EiOPmxG<B@#X
IrI>o@H<&=ME&u=k

diff --git a/regression/strings-smoke-tests/java_append_int/test_append_int.java b/regression/strings-smoke-tests/java_append_int/test_append_int.java
deleted file mode 100644
index 963f3d7c063..00000000000
--- a/regression/strings-smoke-tests/java_append_int/test_append_int.java
+++ /dev/null
@@ -1,11 +0,0 @@
-public class test_append_int
-{
-   public static void main(/*String[] args*/)
-   {
-      StringBuilder diffblue = new StringBuilder();
-      diffblue.append("d");
-      diffblue.append(4);
-      String s = diffblue.toString();
-      assert s.equals("d4");
-   }
-}
diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc
deleted file mode 100644
index c905a3990f6..00000000000
--- a/regression/strings-smoke-tests/java_append_object/test.desc
+++ /dev/null
@@ -1,10 +0,0 @@
-FUTURE
-test_append_object.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
---
-Issue: diffblue/test-gen#82
diff --git a/regression/strings-smoke-tests/java_append_object/test_append_object.class b/regression/strings-smoke-tests/java_append_object/test_append_object.class
deleted file mode 100644
index ed6942a1fa6ddb20c36b528444d598e867e347f5..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 992
zcmZWn*>2N76g`t|9M@^mbPIb6p(Jh7u#`2SEAT>Ekb*$;rE=nF<>J`E3ld+!dwzgt
zij+!Jf_FX&xZ{wfX=VG4=gygP&s~21`SBCLGB#C=VMf8Mg6kYNRKzeNO<tOtNzCDv
ziUNvBq%p5xLB%3U97`%vnBgd^xQ#m;cNxa>y5|YkHyzu1W_o(V5(Wd?VMtU>+w@l$
zqJ`pHhS;WK2!?dcw8eJNY6$m@1k*uFH*JPg-PfBRw)A%BCT`NjagRZ%Hm(0mYTXIk
zrg&k>d(*z~{9V1>7PhhLG!8`5Upmk~=^7?5NwkK!w?|9E3M5#blr7!fFV}t7wD&gx
z(=vpsQ8Dgocz}l-k2E~S6OM|8DxPY{Vw|E&8p%OgG^}8iAvfS!@8|y9bsd)>dtMXA
znuc|3Fk}YzUWIapTs>J-wq8aIr9$oOg-Y?1YbcKjDfOK`$3)>gkPxQ?)IWQ^Xi;yR
zz-O53(V9;AHPyx^8lku7!gwfP*v-J(5@b=&CQnQ31+U0nC&b4<x4bieUec8!%|?2V
z*``GU#4u$D&vb=xQc)TQKcEAeo*m569FEcCvP@34h5n*ovd?6vXm^EHMr(Zj2<)2#
zVw!9sbTTB7JAr;dgk~J5W+N}N(b_R$?~f4QTAc49u|VIu#V+{vA(T=V$wR0eOq8-C
zU1%MQ93w^G(O)t`B#bae+!U7NB<N8v3YBDyP`nh08bzLjSCGL4LXp_Nw25(C4Btx}
sm&vUVu%E|rC>R*arn|^=z++z#i++bXh}h3bGR6_n)@0^aX%oS<e{GZ1nE(I)

diff --git a/regression/strings-smoke-tests/java_append_object/test_append_object.java b/regression/strings-smoke-tests/java_append_object/test_append_object.java
deleted file mode 100644
index 121690451ca..00000000000
--- a/regression/strings-smoke-tests/java_append_object/test_append_object.java
+++ /dev/null
@@ -1,17 +0,0 @@
-public class test_append_object
-{
-   public static void main(/*String[] args*/)
-   {
-      Object diff = "diff";
-      Object blue = "blue";
-
-      StringBuilder buffer = new StringBuilder();
-
-      buffer.append(diff)
-            .append(blue);
-
-      String tmp=buffer.toString();
-      System.out.println(tmp);
-      assert tmp.equals("diffblue");
-   }
-}