Merge pull request #1665 from romainbrenguier/bugfix/string-out-of-bound#TG-1808

Make clear that cbmc version of charAt and substring do not throw OutOfBound TG-1808

Author: Thomas Kiley

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

@@ -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);
+    }
+}

regression/jbmc-strings/SubString01/SubString01.class

@@ -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)