Use a model of String constructor from charArray

The version in the preprocessing was not working correctly for non
constant arrays, so we will get rid of it and it's better to use
a model of the constructor.

Author: romainbrenguier

jbmc/regression/jbmc-strings/java_append_char/test.desc

@@ -4,6 +4,6 @@ test_append_char.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[.*assertion\.1\].* line 16.* SUCCESS$
-^\[.*assertion\.2\].* line 18.* FAILURE$
+^\[.*assertion\.1\].* line 29.* SUCCESS$
+^\[.*assertion\.2\].* line 31.* FAILURE$
 --

jbmc/regression/jbmc-strings/java_append_char/test_append_char.class

@@ -1,20 +1,34 @@
+// This test uses CProverString so should be compiled with
+// javac test_append_char.java ../cprover/CProverString.java ../cprover/CProver.java
+
 public class test_append_char
 {
-  public static void main(boolean b)
-   {
-      char[] diff = {'d', 'i', 'f', 'f'};
-      char[] blue = {'b', 'l', 'u', 'e'};
-
-      StringBuilder buffer = new StringBuilder();
+    public static String ofCharArray(char value[], int offset, int count) {
+      	org.cprover.CProver.assume(value != null);
+	org.cprover.CProver.assume(value.length - count >= offset
+				   && offset >= 0 && count >= 0);
+	StringBuilder builder = new StringBuilder();
+	for(int i = 0; i < count; i++) {
+	    builder.append(value[offset + i]);
+	}
+	return builder.toString();
+    }
 
-      buffer.append(diff)
-            .append(blue);
+    public static String main(boolean b)
+    {
+	char[] diff = {'d', 'i', 'f', 'f'};
+	char[] blue = {'b', 'l', 'u', 'e'};
 
-      String tmp=buffer.toString();
-      System.out.println(tmp);
-      if(b)
-	assert(tmp.equals("diffblue"));
-      else
-	assert(!tmp.equals("diffblue"));
-   }
+	StringBuilder buffer = new StringBuilder();
+	String s = ofCharArray(diff, 0, diff.length);
+	buffer.append(ofCharArray(diff, 0, diff.length))
+	    .append(ofCharArray(blue, 0, blue.length));
+	String tmp=buffer.toString();
+	System.out.println(tmp);
+	if(b)
+	    assert(tmp.equals("diffblue"));
+	else
+	    assert(!tmp.equals("diffblue"));
+	return tmp;
+    }
 }