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