Merge pull request #1539 from romainbrenguier/bugfix/char-array-in-java-strings#TG-58#newpr

TG-58 New PR for Complete rework of string solver to avoid using infinite arrays

Author: peterschrammel

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class

@@ -1,40 +1,52 @@
 public class StringMiscellaneous04
 {
-   public static void main(String[] args)
-   {
-      String s1 = "diffblue";
-      String s2 = "TESTGENERATION";
-      String s3 = "   automated   ";
-
-      assert s1.equals("diffblue");
-      assert s2.equals("TESTGENERATION");
-      assert s3.equals("   automated   ");
-
-      System.out.printf(
-         "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
-      String tmp=s1.replace('f', 'F');
-      assert tmp.equals("diFFblue");
-
-      tmp=s1.toUpperCase();
-      assert tmp.equals("DIFFBLUE");
-
-      tmp=s2.toLowerCase();
-      assert tmp.equals("testgeneration");
-
-      tmp=s3.trim();
-      assert tmp.equals("automated");
-
-      // test toCharArray method
-      char[] charArray = s1.toCharArray();
-      System.out.print("s1 as a character array = ");
-
-      int i=0;
-      for (char character : charArray)
-      {
-         assert character=="diffblue".charAt(i);
-         ++i;
-      }
-
-      System.out.println();
-   }
+    // This is a model of the String.toCharArray method
+    public static char[] toCharArray(String s)
+    {
+        int length=s.length();
+        assert(length<10);
+        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);
+        return arr;
+    }
+
+    public static void main(String[] args)
+    {
+        String s1 = "diffblue";
+        String s2 = "TESTGENERATION";
+        String s3 = "	automated   ";
+
+        assert s1.equals("diffblue");
+        assert s2.equals("TESTGENERATION");
+        assert s3.equals("   automated	 ");
+
+        System.out.printf(
+          "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
+        String tmp=s1.replace('f', 'F');
+        assert tmp.equals("diFFblue");
+
+        tmp=s1.toUpperCase();
+        assert tmp.equals("DIFFBLUE");
+
+        tmp=s2.toLowerCase();
+        assert tmp.equals("testgeneration");
+
+        tmp=s3.trim();
+        assert tmp.equals("automated");
+
+        // test toCharArray method
+        char[] charArray = toCharArray(s1);
+        System.out.print("s1 as a character array = ");
+
+        int i=0;
+        for (char character : charArray)
+        {
+            assert character=="diffblue".charAt(i);
+            ++i;
+        }
+
+        System.out.println();
+    }
 }

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java

@@ -4,5 +4,6 @@ test_append_char.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[.*assertion\.1\].* line 15.* FAILURE$
+^\[.*assertion\.1\].* line 16.* SUCCESS$
+^\[.*assertion\.2\].* line 18.* FAILURE$
 --

regression/jbmc-strings/java_append_char/test.desc

@@ -1,6 +1,6 @@
 public class test_append_char
 {
-   public static void main(/*String[] args*/)
+  public static void main(boolean b)
    {
       char[] diff = {'d', 'i', 'f', 'f'};
       char[] blue = {'b', 'l', 'u', 'e'};
@@ -12,6 +12,9 @@ public static void main(/*String[] args*/)
 
       String tmp=buffer.toString();
       System.out.println(tmp);
-      assert(!tmp.equals("diffblue"));
+      if(b)
+	assert(tmp.equals("diffblue"));
+      else
+	assert(!tmp.equals("diffblue"));
    }
 }

regression/jbmc-strings/java_append_char/test_append_char.class

@@ -3,5 +3,8 @@ test_init.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*assertion.1\].* line 14.* FAILURE$
+assertion.* file test_init.java line 31 .* SUCCESS$
+assertion.* file test_init.java line 33 .* SUCCESS$
+assertion.* file test_init.java line 35 .* FAILURE$
+assertion.* file test_init.java line 37 .* FAILURE$
 --

regression/jbmc-strings/java_append_char/test_append_char.java

@@ -1,18 +1,39 @@
-public class test_init {
+public class test_init
+{
+    // These are models for the constructors of strings from char arrays
+    public static String stringOfCharArray(char arr[])
+    {
+        // We give an arbitrary limit on the size of arrays
+        assert(arr.length<11);
+        StringBuilder sb=new StringBuilder("");
+        for(int i=0; i<arr.length && i<11; i++)
+            sb.append(arr[i]);
+        return sb.toString();
+    }
 
-  public static void main(/*String[] argv*/)
-  {
-     char [] str = new char[10];
-     str[0] = 'H';
-     str[1] = 'e';
-     str[2] = 'l';
-     str[3] = 'l';
-     str[4] = 'o';
-     String s = new String(str);
-     String t = new String(str,1,2);
+    public static String stringOfCharArray(char arr[], int i, int j)
+    {
+        return stringOfCharArray(arr).substring(i, i+j);
+    }
 
-     assert(s.length() != 10 || 
-            !t.equals("el") ||
-            !s.startsWith("Hello"));
-   }
+    public static void main(int i)
+    {
+        char [] str = new char[10];
+        str[0] = 'H';
+        str[1] = 'e';
+        str[2] = 'l';
+        str[3] = 'l';
+        str[4] = 'o';
+        String s = stringOfCharArray(str);
+        String t = stringOfCharArray(str,1,2);
+
+        if(i==0)
+            assert(s.startsWith("Hello"));
+        else if(i==1)
+            assert(t.equals("el"));
+        else if(i==2)
+            assert(!s.startsWith("Hello"));
+        else
+            assert(!t.equals("el"));
+    }
 }

regression/jbmc-strings/java_char_array_init/test.desc

@@ -3,5 +3,6 @@ test_insert_char_array.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*assertion\.1\].* line 12.* FAILURE$
+assertion.* line 28.* SUCCESS$
+assertion.* line 30.* FAILURE$
 --