Adapt existing StringBuilder tests

Activate two tests marked FUTURE that can meanwhile be solved by the string
solver. Also adapt tests so they cannot be solved via constant propagation, and
load the models library.

jbmc/regression/jbmc-strings/StringBuilderCapLen01/StringBuilderCapLen01.java

@@ -1,8 +1,15 @@
 public class StringBuilderCapLen01
 {
-   public static void main(String[] args)
+   public static void test(boolean choice)
    {
-      StringBuilder buffer = new StringBuilder("Diffblue is leader in automatic test case generation");
+      String s =
+        choice
+        ? "Diffblue is leader in automatic test case generation"
+        : "";
+      StringBuilder buffer = new StringBuilder(s);
+
+      if(!choice)
+        return;
 
       assert buffer.toString().equals("Diffblue is leader in automatic test case generation");
       assert buffer.length()==52;

jbmc/regression/jbmc-strings/StringBuilderCapLen01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen01.class
---max-nondet-string-length 1000
+--function StringBuilderCapLen01.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderChars01/StringBuilderChars01.java

@@ -1,10 +1,11 @@
 public class StringBuilderChars01
 {
-   public static void main(String[] args)
+   public static void test(boolean choice)
    {
-      StringBuilder buffer = new StringBuilder("Diffblue Limited");
+      String s = choice ? "Diffblue" : "abcdefgh";
+      StringBuilder buffer = new StringBuilder(s);
 	  
-      assert buffer.toString().equals("Diffblue Limited");
+      assert !choice || buffer.toString().equals("Diffblue");
       assert buffer.charAt(0)!=buffer.charAt(4);
 
       char[] charArray = new char[buffer.length()];
@@ -20,9 +21,9 @@ public class StringBuilderChars01
 
       buffer.setCharAt(0, 'H');
       buffer.setCharAt(6, 'T');
-      assert buffer.toString().equals("HiffBlTe Limited");
+      assert !choice || buffer.toString().equals("HiffblTe");
 
       buffer.reverse();
-      assert buffer.toString().equals("detimiL eTlBffiH");
+      assert !choice || buffer.toString().equals("eTlbffiH");
    }
 }

jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+THOROUGH
 StringBuilderChars01.class
---max-nondet-string-length 1000 --unwind 100
+--function StringBuilderChars01.test --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderChars05/StringBuilderChars05.java

@@ -1,10 +1,11 @@
 public class StringBuilderChars05
 {
-   public static void main(String[] args)
+   public static void test(boolean choice)
    {
-      StringBuilder buffer = new StringBuilder("Diffblue Limited");
+      String s = choice ? "Diffblue Limited" : "Diffblue Unlimited";
+      StringBuilder buffer = new StringBuilder(s);
       buffer.setCharAt(0, 'H');
       buffer.setCharAt(6, 'T');
-      assert buffer.toString().equals("HiffBllTe Limited");
+      assert !choice || buffer.toString().equals("HiffBllTe Limited");
    }
 }

jbmc/regression/jbmc-strings/StringBuilderChars05/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 StringBuilderChars05.class
---max-nondet-string-length 1000 --unwind 100
+--function StringBuilderChars05.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/strings-smoke-tests/java_set_length/test.desc

@@ -1,10 +1,10 @@
 CORE
 test_set_length.class
---max-nondet-string-length 100 --function test_set_length.main
+--function test_set_length.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.1\].* line 9.* SUCCESS$
-^\[.*assertion.2\].* line 9.* SUCCESS$
+^\[.*assertion.2\].* line 10.* SUCCESS$
-^\[.*assertion.3\].* line 10.* FAILURE$
+^\[.*assertion.3\].* line 11.* FAILURE$
 --
 non equal types

jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java

@@ -1,10 +1,11 @@
 public class test_set_length
 {
-   public static void main()
+   public static void main(boolean choice)
    {
-      StringBuilder s = new StringBuilder("abc");
+      String s = choice ? "abc" : "abcxyz";
-      s.setLength(10);
+      StringBuilder sb = new StringBuilder(s);
-      String t = s.toString();
+      sb.setLength(10);
+      String t = sb.toString();
       assert(t.startsWith("abc"));
       assert(t.length() == 10);
       assert(t.length() == 3);