String regression test restructuration

regression/strings-smoke-tests/Makefile

@@ -0,0 +1,9 @@
+
+test:
+	@../test.pl -c ../../../src/cbmc/cbmc
+
+testfuture:
+	@../test.pl -c ../../../src/cbmc/cbmc -CF
+
+testall:
+	@../test.pl -c ../../../src/cbmc/cbmc -CFTK

regression/strings-smoke-tests/java_append_char/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_char.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_char/test_append_char.java

@@ -0,0 +1,17 @@
+public class test_append_char
+{
+   public static void main(/*String[] args*/)
+   {
+      char[] diff = {'d', 'i', 'f', 'f'};
+      char[] blue = {'b', 'l', 'u', 'e'};
+
+      StringBuilder buffer = new StringBuilder();
+
+      buffer.append(diff)
+            .append(blue);
+
+      String tmp=buffer.toString();
+      System.out.println(tmp);
+      assert tmp.equals("diffblue");
+   }
+}

regression/strings-smoke-tests/java_append_int/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_int.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_int/test_append_int.java

@@ -0,0 +1,11 @@
+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");
+   }
+}

regression/strings-smoke-tests/java_append_object/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_object.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_object/test_append_object.java

@@ -0,0 +1,17 @@
+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");
+   }
+}

regression/strings-smoke-tests/java_append_string/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_string.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_string/test_append_string.java

@@ -0,0 +1,14 @@
+public class test_append_string
+{
+   public static void main(/*String[] args*/)
+   {
+      String di = new String("di");
+      StringBuilder diff = new StringBuilder();
+      diff.append(di);
+      diff.append("ff");
+      System.out.println(diff);
+      String s = diff.toString();
+      System.out.println(s);
+      assert s.equals("diff");
+   }
+}

regression/strings-smoke-tests/java_case/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_case.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_case/test_case.java

@@ -0,0 +1,12 @@
+public class test_case
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("Ab");
+      String l = s.toLowerCase();
+      String u = s.toUpperCase();
+      assert(l.equals("ab"));
+      assert(u.equals("AB"));
+      assert(s.equalsIgnoreCase("aB"));
+   }
+}

regression/strings-smoke-tests/java_char_array/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_char_array.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_char_array/test_char_array.java

@@ -0,0 +1,13 @@
+public class test_char_array
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = "abc";
+      char [] str = s.toCharArray();
+      char c = str[2];
+      char a = s.charAt(0);
+      assert(str.length == 3);
+      assert(a == 'a');
+      assert(c == 'c');
+   }
+}

regression/strings-smoke-tests/java_char_array_init/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_init.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_char_array_init/test_init.java

@@ -0,0 +1,21 @@
+public class test_init {
+
+  public static void main(/*String[] argv*/)
+  {
+     char [] str = new char[10];
+     str[0] = 'H';
+     str[1] = 'e';
+     str[2] = 'l';
+     str[3] = 'l';
+     str[4] = 'o';
+     String s = new String(str);
+     String t = new String(str,1,2);
+
+     System.out.println(s.length());
+     assert(s.length() == 10);
+     System.out.println(s);
+     System.out.println(t);
+     assert(t.equals("el"));
+     assert(s.startsWith("Hello"));
+   }
+}

regression/strings-smoke-tests/java_char_at/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_char_at.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_char_at/test_char_at.java

@@ -0,0 +1,7 @@
+public class test_char_at {
+
+  public static void main(/*String[] argv*/) {
+    String s = new String("abc");
+    assert(s.charAt(2)=='c');
+  }
+}

regression/strings-smoke-tests/java_code_point/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_code_point.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_code_point/test_code_point.java

@@ -0,0 +1,14 @@
+public class test_code_point
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = "!𐤇𐤄𐤋𐤋𐤅";
+      assert(s.codePointAt(1) == 67847);
+      assert(s.codePointBefore(3) == 67847);
+      assert(s.codePointCount(1,5) >= 2);
+      assert(s.offsetByCodePoints(1,2) >= 3);
+      StringBuilder sb = new StringBuilder();
+      sb.appendCodePoint(0x10907);
+      assert(s.charAt(1) == sb.charAt(0));
+   }
+}

regression/strings-smoke-tests/java_compare/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_compare.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_compare/test_compare.java

@@ -0,0 +1,9 @@
+public class test_compare
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s1 = "ab";
+      String s2 = "aa";
+      assert(s1.compareTo(s2) == 1);
+   }
+}

regression/strings-smoke-tests/java_concat/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_concat.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 10.* SUCCESS$
+^\[.*assertion.2\].* line 11.* FAILURE$
+--

regression/strings-smoke-tests/java_concat/test_concat.java

@@ -0,0 +1,13 @@
+public class test_concat
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("pi");
+      int i = s.length();
+      String t = new String("ppo");
+      String u = s.concat(t);
+      char c = u.charAt(i);
+      assert(c == 'p');
+      assert(c == 'o');
+   }
+}

regression/strings-smoke-tests/java_contains/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_contains.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--

regression/strings-smoke-tests/java_contains/test_contains.java

@@ -0,0 +1,11 @@
+public class test_contains
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("Abc");
+      String u = "bc";
+      String t = "ab";
+      assert(s.contains(u));
+      assert(s.contains(t));
+   }
+}

regression/strings-smoke-tests/java_delete/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_delete.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_delete/test_delete.java

@@ -0,0 +1,10 @@
+public class test_delete
+{
+   public static void main(/*String[] argv*/)
+   {
+      StringBuilder s = new StringBuilder("Abc");
+      s.delete(1,2);
+      String str = s.toString();
+      assert(str.equals("Ac"));
+   }
+}

regression/strings-smoke-tests/java_delete_char_at/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_delete_char_at.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java

@@ -0,0 +1,11 @@
+public class test_delete_char_at
+{
+   public static void main(/*String[] argv*/)
+   {
+      StringBuilder s = new StringBuilder();
+      s.append("Abc");
+      s.deleteCharAt(1);
+      String str = s.toString();
+      assert(str.equals("Ac"));
+   }
+}

regression/strings-smoke-tests/java_empty/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_empty.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_empty/test_empty.java

@@ -0,0 +1,8 @@
+public class test_empty
+{
+   public static void main(/*String[] argv*/)
+   {
+      String empty = "";
+      assert(empty.isEmpty());
+   }
+}

regression/strings-smoke-tests/java_endswith/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_endswith.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 9.* SUCCESS$
+^\[.*assertion.2\].* line 10.* FAILURE$
+--

regression/strings-smoke-tests/java_endswith/test_endswith.java

@@ -0,0 +1,12 @@
+public class test_endswith
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("Abcd");
+      String suff = "cd";
+      String bad_suff = "bc";
+
+      assert(s.endsWith(suff));
+      assert(s.endsWith(bad_suff));
+   }
+}

regression/strings-smoke-tests/java_equal/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_equal.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* FAILURE$
+^\[.*assertion.2\].* line 9.* SUCCESS$
+--

regression/strings-smoke-tests/java_equal/test_equal.java

@@ -0,0 +1,11 @@
+public class test_equal
+{
+   public static void main(String[] argv)
+   {
+      String s = new String("pi");
+      String t = new String("po");
+      String u = "po";
+      assert(s.equals(t));
+      assert(t.equals(u));
+   }
+}

regression/strings-smoke-tests/java_float/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_float.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--