Use CProverString functions in strings-smoke-tests

We replace calls to charAt/substring by corresponding CProverString functions.

Author: romainbrenguier

regression/strings-smoke-tests/java_append_string/test_append_string.class

@@ -20,7 +20,7 @@ public static void check(StringBuilder sb, String str)
             sb.append(str, 2, 4);
             String res = sb.toString();
             assert(res.startsWith(init));
-            assert(res.endsWith(str.substring(2, 4)));
+            assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));
             assert(res.length() == init.length() + 2);
             assert(!res.equals("foobarfuz"));
         }

regression/strings-smoke-tests/java_append_string/test_append_string.java

@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
         char arr[] = new char[s.length()];
         // We limit arbitrarly the loop unfolding to 5
         for(int i = 0; i < length && i < 5; i++)
-        arr[i] = s.charAt(i);
+            arr[i] = org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
@@ -17,7 +17,7 @@ public static void main(int i)
         String s = "abc";
         char [] str = toCharArray(s);
         char c = str[2];
-        char a = s.charAt(0);
+        char a = org.cprover.CProverString.charAt(s, 0);
         assert(str.length == 3);
         assert(a == 'a');
         assert(c == 'c');

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

@@ -2,6 +2,6 @@ public class test_char_at {
 
   public static void main(/*String[] argv*/) {
     String s = new String("abc");
-    assert(s.charAt(2)=='c');
+    assert(org.cprover.CProverString.charAt(s, 2)=='c');
   }
 }

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

@@ -9,6 +9,6 @@ public static void main(/*String[] argv*/)
       assert(s.offsetByCodePoints(1,2) >= 3);
       StringBuilder sb = new StringBuilder();
       sb.appendCodePoint(0x10907);
-      assert(s.charAt(1) == sb.charAt(0));
+      assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));
    }
 }

regression/strings-smoke-tests/java_char_at/test_char_at.class

@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c == 'o');
    }

regression/strings-smoke-tests/java_char_at/test_char_at.java

@@ -3,11 +3,11 @@ public class test_set_char_at
    public static void main(/*String[] argv*/)
    {
       String s = new String("Abc");
-      char c = s.charAt(1);
+      char c = org.cprover.CProverString.charAt(s, 1);
       StringBuilder sb = new StringBuilder(s);
       sb.setCharAt(1,'w');
       s = sb.toString();
       assert(s.equals("Awc"));
-      assert(s.charAt(2)=='c');
+      assert(org.cprover.CProverString.charAt(s, 2)=='c');
    }
 }

regression/strings-smoke-tests/java_code_point/test_code_point.class

@@ -3,10 +3,10 @@ public class test_substring
    public static void main(/*String[] argv*/)
    {
       String abcdef = "AbcDef";
-      String cde = abcdef.substring(2,5);
-      char c = cde.charAt(0);
-      char d = cde.charAt(1);
-      char e = cde.charAt(2);
+      String cde = org.cprover.CProverString.substring(abcdef, 2,5);
+      char c = org.cprover.CProverString.charAt(cde, 0);
+      char d = org.cprover.CProverString.charAt(cde, 1);
+      char e = org.cprover.CProverString.charAt(cde, 2);
       assert(c == 'c');
       assert(d == 'D');
       assert(e == 'e');