Improve the StringBuilder constructor tests

Split the tests for the different constructors, add assertions that
are supposed to fail, and activate the tests that can be.

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class

@@ -1,13 +1,33 @@
 public class StringBuilderConstructors01
 {
-   public static void main(String[] args)
-   {
-      StringBuilder buffer1 = new StringBuilder();
-      StringBuilder buffer2 = new StringBuilder(10);
-      StringBuilder buffer3 = new StringBuilder("diffblue");
-
-      assert buffer1.length()==0;
-      assert buffer2.length()==0;
-      assert buffer3.length()>0;
-   }
+  public static void noArgPass() {
+    StringBuilder buffer1 = new StringBuilder();
+    assert buffer1.length() == 0;
+  }
+
+  public static void noArgFail() {
+    StringBuilder buffer1 = new StringBuilder();
+    assert buffer1.length() != 0;
+  }
+
+  public static void capacityPass() {
+    StringBuilder buffer2 = new StringBuilder(10);
+    assert buffer2.length() == 0;
+  }
+
+  public static void capacityFail() {
+
+    StringBuilder buffer2 = new StringBuilder(10);
+    assert buffer2.length() != 0;
+  }
+
+  public static void stringPass() {
+    StringBuilder buffer3 = new StringBuilder("diffblue");
+    assert buffer3.length() == 8;
+  }
+
+  public static void stringFail() {
+    StringBuilder buffer3 = new StringBuilder("diffblue");
+    assert buffer3.length() != 8;
+  }
 }

jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java

@@ -0,0 +1,11 @@
+KNOWNBUG
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.capacityFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is not working currently because the StringBuilder constructor with
+capacity argument is not modelled.

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.capacityPass --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This is not working currently because the StringBuilder constructor with
+capacity argument is not modelled.

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc

@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.noArgFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 StringBuilderConstructors01.class
---max-nondet-string-length 1000
+--function StringBuilderConstructors01.noArgPass --max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc renamed to jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc

@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.stringFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc

@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.stringPass --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring