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");
+   }
+}