Update regression tests to use string primitives

Instead of calling the original Java string methods, regression tests
now call the jbmc string primitives.

Not all string methods have a jbmc counterpart yet. It is limited to
methods that throw exceptions.

Author: Joel Allred

regression/jbmc-strings/cprover/CProverString.class

@@ -8,6 +8,29 @@ public static char charAt(String s, int i) {
             return '\u0000';
     }
 
+    public static int codePointAt(String s, int index) {
+        return s.codePointAt(index);
+    }
+
+    public static int codePointBefore(String s, int index) {
+        return s.codePointBefore(index);
+    }
+
+    public static int codePointCount(
+            String s, int beginIndex, int endIndex) {
+        return s.codePointCount(beginIndex, endIndex);
+    }
+
+    public static int offsetByCodePoints(
+            String s, int index, int codePointOffset) {
+        return s.offsetByCodePoints(index, codePointOffset);
+    }
+
+    public static CharSequence subSequence(
+            String s, int beginIndex, int endIndex) {
+        return s.subSequence(beginIndex, endIndex);
+    }
+
     public static String substring(String s, int i) {
         if (i <= 0)
             return s;
@@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) {
             return "";
         return s.substring(i, j);
     }
+
+    public static StringBuilder append(
+            StringBuilder sb, CharSequence cs, int i, int j) {
+        return sb.append(cs, i, j);
+    }
+
+    public static StringBuilder delete(StringBuilder sb, int start, int end) {
+        return sb.delete(start, end);
+    }
+
+    public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
+        return sb.deleteCharAt(index);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, String str) {
+        return sb.insert(offset, str);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, boolean b) {
+        return sb.insert(offset, b);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, char c) {
+        return sb.insert(offset, c);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, int i) {
+        return sb.insert(offset, i);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, long l) {
+        return sb.insert(offset, l);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, float f) {
+        return sb.insert(offset, f);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, double d) {
+        return sb.insert(offset, d);
+    }
+
+    public static void setLength(StringBuffer sb, int newLength) {
+        sb.setLength(newLength);
+    }
+
+    public static char charAt(StringBuffer sb, int index) {
+        return sb.charAt(index);
+    }
+
+    public static void setCharAt(StringBuffer sb, int index, char c) {
+        sb.setCharAt(index, c);
+    }
+
+    public static StringBuffer delete(
+            StringBuffer sb, int start, int end) {
+        return sb.delete(start, end);
+    }
+
+    public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
+        return sb.deleteCharAt(index);
+    }
+
+    public static String substring(StringBuffer sb, int start, int end) {
+        return sb.substring(start, end);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, String str) {
+        return sb.insert(offset, str);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, boolean b) {
+        return sb.insert(offset, b);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, char c) {
+        return sb.insert(offset, c);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, int i) {
+        return sb.insert(offset, i);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, long l) {
+        return sb.insert(offset, l);
+    }
 }

regression/jbmc-strings/cprover/CProverString.java

@@ -3,7 +3,7 @@ public class test_delete
    public static void main(/*String[] argv*/)
    {
       StringBuilder s = new StringBuilder("Abc");
-      s.delete(1,2);
+      org.cprover.CProverString.delete(s,1,2);
       String str = s.toString();
       assert(!str.equals("Ac"));
    }

regression/jbmc-strings/java_delete/test_delete.class

@@ -4,7 +4,7 @@ public static void main(/*String[] argv*/)
    {
       StringBuilder s = new StringBuilder();
       s.append("Abc");
-      s.deleteCharAt(1);
+      org.cprover.CProverString.deleteCharAt(s, 1);
       String str = s.toString();
       assert(!str.equals("Ac"));
    }

regression/jbmc-strings/java_delete/test_delete.java

@@ -3,7 +3,7 @@ public class test_insert_char
    public static void main(/*String[] argv*/)
    {
       StringBuilder sb = new StringBuilder("ac");
-      sb.insert(1, 'b');
+      org.cprover.CProverString.insert(sb, 1, 'b');
       String s = sb.toString();
       assert(!s.equals("abc"));
    }

regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class

@@ -3,6 +3,6 @@ test_insert_char_array.class
 --refine-strings --string-max-length 1000 --function test_insert_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion.* line 28.* SUCCESS$
-assertion.* line 30.* FAILURE$
+assertion.* line 26.* SUCCESS$
+assertion.* line 28.* FAILURE$
 --