Tests for CProverString.append with start/end args

This test the CProverString.append function when start_index and
end_index arguments are proivided.

Author: romainbrenguier

regression/jbmc-strings/StringConcat_StringII/Test.class

@@ -0,0 +1,40 @@
+// This test uses CProverString so should be compiled with
+// javac Test.java ../cprover/CProverString.java
+import org.cprover.CProverString;
+
+class Test {
+    public void testSuccess(String s, String t, int start, int end) {
+        // Filter
+        if (s == null || t == null)
+            return;
+
+        // Act
+        StringBuilder sb = new StringBuilder(s);
+        String result = CProverString.append(sb, t, start, end).toString();
+
+        // Arrange
+        StringBuilder reference = new StringBuilder(s);
+        if(start < 0)
+            start = 0;
+        for (int i = start; i < end && i < t.length(); i++)
+            reference.append(org.cprover.CProverString.charAt(t, i));
+
+        // Assert
+        assert result.equals(reference.toString());
+    }
+
+    public void testFail(int i) {
+        // Arrange
+        StringBuilder sb = new StringBuilder("foo");
+
+        // Act
+        CProverString.append(sb, "bar", 0, 1);
+        CProverString.append(sb, "bar", 0, 4);
+        CProverString.append(sb, "foo", -1, 0);
+        CProverString.append(sb, "foo", -10, -1);
+        CProverString.append(sb, "bar", -10, 25);
+
+        // Assert
+        assert !sb.toString().equals("foobbarbar");
+    }
+}

regression/jbmc-strings/StringConcat_StringII/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 23 .*: SUCCESS
+--
+^warning: ignoring

regression/jbmc-strings/StringConcat_StringII/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 38 .*: FAILURE
+--
+^warning: ignoring