Restructuration of tests on strings

Add test java_intern
Adapt test.desc to new output format
Make more robust java tests.
Add test for parseint.

Correction in the hacks to use refined strings in C programs

Add smoke tests for java string support
Quick set of tests.
Created by modifying the existing development tests.
Longer tests are run when using 'make testall'.
Format of java files was adapted.
No change to the validation tests (written by Lucas Cordeiro).

Update smoke tests

Add a series of performance tests that check that the negation of the
assertions found in the smoke tests indeed fail.

Update java_char_array_init/test_init.class

Add first fixed_bugs test
For bug #95

Update test description with new option name
String refinement option name has changed to --refine-strings

Formatting in cprover-string-hack.h

Move smoke tests to regression folder.

Move fixed bugs tests to strings folder

Move string perfomance tests to strings directory

These are not really performance tests, only tests that are longer than
the smoke tests.

Adapt Makefile for new location of smoke tests

Author: Joel Allred

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.class

@@ -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_char/test_append_char.java

@@ -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.desc

@@ -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_int/test_append_int.class

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

regression/strings-smoke-tests/java_append_int/test_append_int.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_object/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_object/test_append_object.class

@@ -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_append_object/test_append_object.java

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

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

@@ -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_append_string/test_append_string.class

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

regression/strings-smoke-tests/java_append_string/test_append_string.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_case/test.desc

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

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

@@ -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_case/test_case.java

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

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

@@ -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_char_array/test_char_array.class

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

regression/strings-smoke-tests/java_char_array/test_char_array.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_char_array_init/test.desc

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

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

@@ -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_char_array_init/test_init.java

@@ -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_char_at/test.desc

@@ -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_char_at/test_char_at.class

@@ -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_char_at/test_char_at.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_code_point/test.desc

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

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

@@ -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_code_point/test_code_point.java

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

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

@@ -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_compare/test_compare.class

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

regression/strings-smoke-tests/java_compare/test_compare.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_concat/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_concat/test_concat.class

@@ -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_concat/test_concat.java

@@ -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_contains/test.desc

@@ -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_contains/test_contains.class

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