Use CProverString function in jbmc tests

charAt and substring are replaced by CProver functions

Author: romainbrenguier

regression/jbmc-strings/StringLastIndexOf/Test.class

@@ -13,7 +13,7 @@ public void check(String input_String1, String input_String2, int i) {
                 // Contradiction with the previous condition (should fail).
                 assert "foo".lastIndexOf("") != 3;
             } else if (i == 2 && input_String2.length() > 0) {
-                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                int lio = input_String1.lastIndexOf(org.cprover.CProverString.charAt(input_String2, 0), fromIndex);
                 if (input_String2.length() == 0)
                     assert lio == fromIndex;
             } else if (i == 3) {

regression/jbmc-strings/StringLastIndexOf/Test.java

@@ -8,19 +8,19 @@ public static char[] toCharArray(String s)
         char arr[]=new char[s.length()];
         // We limit arbitrarly the loop unfolding to 10
         for(int i=0; i<length && i<10; i++)
-            arr[i]=s.charAt(i);
+            arr[i]=org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
     public static void main(String[] args)
     {
         String s1 = "diffblue";
         String s2 = "TESTGENERATION";
-        String s3 = "	automated   ";
+        String s3 = "   automated   ";
 
         assert s1.equals("diffblue");
         assert s2.equals("TESTGENERATION");
-        assert s3.equals("   automated	 ");
+        assert s3.equals("   automated   ");
 
         System.out.printf(
           "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
@@ -43,7 +43,7 @@ public static void main(String[] args)
         int i=0;
         for (char character : charArray)
         {
-            assert character=="diffblue".charAt(i);
+            assert character==org.cprover.CProverString.charAt("diffblue", i);
             ++i;
         }
 

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class

@@ -1,13 +1,12 @@
 public class SubString01
 {
-   public static void main(String[] args)
-   {
-      String letters = "automatictestcasegenerationatdiffblue";
+    public static void main(String[] args)
+    {
+        String letters = "automatictestcasegenerationatdiffblue";
 
-      String tmp=letters.substring(20);
-      assert tmp.equals("erationatdiffblue");
-
-      tmp=letters.substring(9, 13);
-      assert tmp.equals("test");
-   }
+        String tmp=org.cprover.CProverString.substring(letters, 20);
+        assert tmp.equals("erationatdiffblue");
+        tmp=org.cprover.CProverString.substring(letters, 9, 13);
+        assert tmp.equals("test");
+    }
 }

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java

@@ -13,7 +13,7 @@ public static String stringOfCharArray(char arr[])
 
     public static String stringOfCharArray(char arr[], int i, int j)
     {
-        return stringOfCharArray(arr).substring(i, i+j);
+        return org.cprover.CProverString.substring(stringOfCharArray(arr), i, i+j);
     }
 
     public static void main(int i)

regression/jbmc-strings/SubString01/SubString01.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 != 'p');
    }