Add a CProverString class for string-smoke-tests

This defines useful string functions replacing standard java functions
that cannot be directly supported in cbmc because of exception throwing.

Author: romainbrenguier

regression/strings-smoke-tests/cprover/CProverString.class

@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}