From 799898f2114057e6d74ba77d866b96daf37153f0 Mon Sep 17 00:00:00 2001
From: Joel Allred <joel.allred@diffblue.com>
Date: Mon, 1 Jul 2019 15:17:26 +0100
Subject: [PATCH 1/2] Rename StringBuilder test folder

---
 .../test.class                                      | Bin
 .../test.desc                                       |   0
 .../test.java                                       |   0
 3 files changed, 0 insertions(+), 0 deletions(-)
 rename jbmc/regression/jbmc-strings/{bug-test-gen-095 => StringBuilderAppend03}/test.class (100%)
 rename jbmc/regression/jbmc-strings/{bug-test-gen-095 => StringBuilderAppend03}/test.desc (100%)
 rename jbmc/regression/jbmc-strings/{bug-test-gen-095 => StringBuilderAppend03}/test.java (100%)

diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.class b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class
similarity index 100%
rename from jbmc/regression/jbmc-strings/bug-test-gen-095/test.class
rename to jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc
rename to jbmc/regression/jbmc-strings/StringBuilderAppend03/test.desc
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.java b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java
similarity index 100%
rename from jbmc/regression/jbmc-strings/bug-test-gen-095/test.java
rename to jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java

From 62ceb1bd82bf1d9ce6f340ca566e06d1020f1ea1 Mon Sep 17 00:00:00 2001
From: Joel Allred <joel.allred@diffblue.com>
Date: Mon, 1 Jul 2019 16:07:53 +0100
Subject: [PATCH 2/2] Improve and enable StringBuilder.append() tests

---
 .../StringBuilderAppend03/test.class          | Bin 822 -> 877 bytes
 .../StringBuilderAppend03/test.desc           |   8 -------
 .../StringBuilderAppend03/test.java           |  20 ++++++++++++------
 .../StringBuilderAppend03/test1.desc          |  10 +++++++++
 .../StringBuilderAppend03/test2.desc          |  10 +++++++++
 .../StringBuilderAppend03/test3.desc          |  10 +++++++++
 6 files changed, 43 insertions(+), 15 deletions(-)
 delete mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppend03/test.desc
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
 create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc

diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class
index 3895d218c3d8e77e3a8cabefd360d149dd58cf12..fe13d89a5c907062a4daa4cf8d907478e906df4f 100644
GIT binary patch
delta 543
zcmYL`y>HV{6vcnfcKjUY84|ZN{h(>fM<|UUg(kp+5Oe{-03E8r6e%GDRR$%7wL4ps
ziAv0{0+K6H1Uvr=e*%bWqrh@Mj?TO1-1}1Zr+fFu?=Rng7B_rOQq!#XSgd+fvb>gs
zGahGs&T+m-KwWde$ETJd>za!`8#FZ0czavB@r$_IOC~SX;`l?^S<ze?f34pPnNd`q
zcV2gz`<=Mo+)0LmxPSZAV87cN8bYdu%QOv}Tv1q0`|{3kl`TV=%4Ah7%^GpIrErqo
zDABYH*SJ2pr`9KL)RU4wN;<=2v^z+iiFDOGR(QR*`xkJm)<Gbvfhx~u^Q5v-qB<jS
zR=Q=$N^)W22=y@|a!R6`gNh<^RHe?S@8qd1`Oz`fp3v?4jnGLc>^4%|2T`a~yth<7
zQ9NYx7=Q1G()Z{f<CrPFFvW9LY1(DNRxVr@NpU056~9_AkD7FmoV`tnJMs+=Wutjv
z1=zocGz*%=xj=|Z|JG{d{-F}KgOn48Xy-kS{h8u_sp*c{r~;O`m0jX=?qvB73pG!9

delta 502
zcmY+9OKVe66otQYUnjXaYI1GUsD1d1dDKK}bkd1J9TX}Zh)NX)SBWvDrg(F8;-J4F
zWFq+kj#an;3knYXE8<U3+$W&L$zJO$)>(V)pFtLEeE<FV3((<a$Z?i5%OMUcIf@p~
z+Ho$A;e3t@As4x%sfL8sc{!v;UDFtCZiL>;xIa*oYmZ0os@}4uIr>(0OGKj|i<>1@
z4OeIx+FUi9pr~-3_rzql#+stC8^4L$d-0&xzC9dvleE7-xRWINiNZ^}!&GzKNXHxF
z`>Ix+uWcRK@1;q9&|9xR7{66dR)X%U*YVy^@t<e=>2CK~x?X=Y4xG+`kvl;ZE4GI)
z7lrhcc~V|Wf=bYDOi>@KkvW;cOjP8Vr!3rBU*O4SXdmM2G~Bf*?p8DMGW>_ljNtA^
z^n|(9D3_6+P&g#qnNm3TYEzwAY8hX+PeJk{Gz;Wt$&Lk43#ebTG!@M$kx&0?*qK#<
gQe-lYP0-$ZJogj&DEDt$o8#k{TlS_iv$czV0N)x*B>(^b

diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.desc
deleted file mode 100644
index 25b7c86bea2..00000000000
--- a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-FUTURE
-test.class
---max-nondet-string-length 1000
-^EXIT=10$
-^SIGNAL=0$
-\[.*assertion\.1\] .* line 8 .* FAILURE
-^VERIFICATION FAILED$
---
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java
index a6910527551..3244e91fc6d 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java
@@ -1,10 +1,16 @@
 public class test
 {
-   public static void main(String[] args)
-   {
-      StringBuilder sb = new StringBuilder(args[0]);
-      sb.append("Z");
-      String s = sb.toString();
-      assert(s.equals("fg"));
-   }
+    public static void nondet(String stringArg)
+    {
+        StringBuilder sb = new StringBuilder(stringArg);
+        sb.append("Z");
+        String s = sb.toString();
+        if (s.startsWith("fg")) {
+            assert false;
+        } else if (s.endsWith("Z")) {
+            assert false;
+        } else {
+            assert false;
+        }
+    }
 }
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
new file mode 100644
index 00000000000..0e6da5a1c97
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+\[.*assertion\.1\] .* line 9 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
new file mode 100644
index 00000000000..10c1a6b6a64
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+\[.*assertion\.2\] .* line 11.* FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
new file mode 100644
index 00000000000..ac6bf282fb0
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+\[.*assertion\.3\] .* line 13.* SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.