Better test for String.toCharArray

We now have in the test both assertions that should pass and
assertions that should fail. This is to make sure our tests do not
pass just because CBMC would be biased in one direction.

Author: romainbrenguier

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

@@ -1,7 +1,13 @@
 CORE
 test_char_array.class
 --refine-strings
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+.*assertion.* test_char_array.java line 9 .* SUCCESS$
+.*assertion.* test_char_array.java line 10 .* SUCCESS$
+.*assertion.* test_char_array.java line 11 .* SUCCESS$
+.*assertion.* test_char_array.java line 13 .* FAILURE$
+.*assertion.* test_char_array.java line 15 .* FAILURE$
+.*assertion.* test_char_array.java line 17 .* FAILURE$
+^VERIFICATION FAILED$
 --

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

@@ -1,6 +1,6 @@
 public class test_char_array
 {
-   public static void main(/*String[] argv*/)
+   public static void main(int i)
    {
       String s = "abc";
       char [] str = s.toCharArray();
@@ -9,5 +9,11 @@ public static void main(/*String[] argv*/)
       assert(str.length == 3);
       assert(a == 'a');
       assert(c == 'c');
+      if(i==0)
+          assert(str.length != 3);
+      if(i==2)
+          assert(a != 'a');
+      if(i==3)
+          assert(c != 'c');
    }
 }