Regression: include model for string to char array

Using model of char array functions in tests.
Also correct java_if test description file.
Remove java_object_allocation test, this should be replaced by unit tests.
Removing java_append_char test duplicate of the one in
string-smoke-test.
Including models of char array functions for some string
regression tests.

Author: romainbrenguier

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

@@ -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_char_array_init/test.desc

@@ -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_init.class

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

regression/jbmc-strings/java_char_array_init/test_init.java

@@ -1,14 +1,30 @@
 public class test_insert_char_array
 {
-   public static void main(/*String[] argv*/)
-   {
-      StringBuilder sb = new StringBuilder("ad");
-      char[] array = new char[2];
-      array[0] = 'b';
-      array[1] = 'c';
-      sb.insert(1, array);
-      String s = sb.toString();
-      System.out.println(s);
-      assert(!s.equals("abcd"));
-   }
+    // These are models of the String methods manipulating char arrays
+    public static String stringOfCharArray(char arr[])
+    {
+        StringBuilder sb=new StringBuilder("");
+        for(int i=0; i<arr.length; i++)
+            sb.append(arr[i]);
+        return sb.toString();
+    }
+    public static void insert(StringBuilder sb, int pos, char arr[])
+    {
+        String s=stringOfCharArray(arr);
+        sb.insert(pos, s);
+    }
+    public static void main(int i)
+    {
+        StringBuilder sb = new StringBuilder("ad");
+        char[] array = new char[2];
+        array[0] = 'b';
+        array[1] = 'c';
+        insert(sb, 1, array);
+        String s = sb.toString();
+        System.out.println(s);
+        if(i==0)
+            assert(s.equals("abcd"));
+        else
+            assert(!s.equals("abcd"));
+    }
 }

regression/jbmc-strings/java_insert_char_array/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_append_char.class
 --refine-strings --string-max-length 1000
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+assertion.* file test_append_char.java line 23 .* SUCCESS
+assertion.* file test_append_char.java line 25 .* FAILURE
 --

regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class

@@ -1,17 +1,27 @@
 public class test_append_char
 {
-   public static void main(/*String[] args*/)
-   {
-      char[] diff = {'d', 'i', 'f', 'f'};
-      char[] blue = {'b', 'l', 'u', 'e'};
+    public static String ofCharArray(char arr[])
+    {
+        StringBuilder sb = new StringBuilder("");
+        for(int i = 0; i < arr.length; i++)
+            sb.append(arr[i]);
+        return sb.toString();
+    }
+    public static void main(String[] args)
+    {
+        char[] diff = {'d', 'i', 'f', 'f'};
+        char[] blue = {'b', 'l', 'u', 'e'};
 
-      StringBuilder buffer = new StringBuilder();
+        StringBuilder buffer = new StringBuilder();
 
-      buffer.append(diff)
-            .append(blue);
+        buffer.append(ofCharArray(diff))
+              .append(ofCharArray(blue));
 
-      String tmp=buffer.toString();
-      System.out.println(tmp);
-      assert tmp.equals("diffblue");
-   }
+        String tmp=buffer.toString();
+        System.out.println(tmp);
+        if(args.length == 0)
+            assert tmp.equals("diffblue");
+        else
+            assert !tmp.equals("diffblue");
+    }
 }

regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java

@@ -3,11 +3,12 @@ test_char_array.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-.*assertion.* test_char_array.java line 9 .* SUCCESS$
-.*assertion.* test_char_array.java line 10 .* SUCCESS$
-.*assertion.* test_char_array.java line 11 .* SUCCESS$
-.*assertion.* test_char_array.java line 13 .* FAILURE$
-.*assertion.* test_char_array.java line 15 .* FAILURE$
-.*assertion.* test_char_array.java line 17 .* FAILURE$
+.*assertion.* test_char_array.java line 7 .* SUCCESS$
+.*assertion.* test_char_array.java line 21 .* SUCCESS$
+.*assertion.* test_char_array.java line 22 .* SUCCESS$
+.*assertion.* test_char_array.java line 23 .* SUCCESS$
+.*assertion.* test_char_array.java line 25 .* FAILURE$
+.*assertion.* test_char_array.java line 27 .* FAILURE$
+.*assertion.* test_char_array.java line 29 .* FAILURE$
 ^VERIFICATION FAILED$
 --

regression/strings-smoke-tests/java_append_char/test.desc

@@ -1,19 +1,31 @@
 public class test_char_array
 {
-   public static void main(int i)
-   {
-      String s = "abc";
-      char [] str = s.toCharArray();
-      char c = str[2];
-      char a = s.charAt(0);
-      assert(str.length == 3);
-      assert(a == 'a');
-      assert(c == 'c');
-      if(i==0)
-          assert(str.length != 3);
-      if(i==2)
-          assert(a != 'a');
-      if(i==3)
-          assert(c != 'c');
-   }
+    // This is a model of the String.toCharArray method
+    public static char[] toCharArray(String s)
+    {
+        int length = s.length();
+        assert(length < 5);
+        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);
+        return arr;
+    }
+
+    public static void main(int i)
+    {
+        String s = "abc";
+        char [] str = toCharArray(s);
+        char c = str[2];
+        char a = s.charAt(0);
+        assert(str.length == 3);
+        assert(a == 'a');
+        assert(c == 'c');
+        if(i == 0)
+            assert(str.length != 3);
+        if(i == 2)
+            assert(a != 'a');
+        if(i == 3)
+            assert(c != 'c');
+    }
 }

regression/strings-smoke-tests/java_append_char/test_append_char.class

@@ -3,7 +3,7 @@ test.class
 --refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*assertion.1\].* line 12.* SUCCESS$
-^\[.*assertion.2\].* line 13.* FAILURE$
+^\[.*assertion.1\].* line 13.* SUCCESS$
+^\[.*assertion.2\].* line 15.* FAILURE$
 --
 $ignoring\s*char\s*array

regression/strings-smoke-tests/java_append_char/test_append_char.java

@@ -1,7 +1,8 @@
 CORE
 test_insert_char_array.class
 --refine-strings --string-max-length 1000
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+assertion.* file test_insert_char_array.java line 20 .* SUCCESS$
+assertion.* file test_insert_char_array.java line 22 .* FAILURE$
 --

regression/strings-smoke-tests/java_char_array/test.desc

@@ -1,14 +1,24 @@
 public class test_insert_char_array
 {
-   public static void main(/*String[] argv*/)
-   {
-      StringBuilder sb = new StringBuilder("ad");
-      char[] array = new char[2];
-      array[0] = 'b';
-      array[1] = 'c';
-      sb.insert(1, array);
-      String s = sb.toString();
-      System.out.println(s);
-      assert(s.equals("abcd"));
-   }
+    public static void insert(StringBuilder sb, int offset, char[] arr)
+    {
+        assert(arr.length<5);
+        for(int i=0; i<arr.length && i<5; i++)
+            sb.insert(offset+i, arr[i]);
+    }
+
+    public static void main(int i)
+    {
+        StringBuilder sb = new StringBuilder("ad");
+        char[] array = new char[2];
+        array[0] = 'b';
+        array[1] = 'c';
+        insert(sb, 1, array);
+        String s = sb.toString();
+        System.out.println(s);
+        if(i==0)
+            assert(s.equals("abcd"));
+        else
+            assert(!s.equals("abcd"));
+    }
 }