Regression test for the string-refine option

We are going to add a string-refine option to CBMC, (instead a pass
option as used in previous version of the tests).
We changed the test description file accordingly and added a few
extra tests (for java char arrays).

Also changed the flag in string regression from CORE to FUTURE:
Since the string solver is not yet part of this branch, we mark the
tests for string functions as FUTURE. They will be changed to CORE
once the corresponding features are integrated in CBMC.
I also changed the Makefile for being able to test tests marked as
future.

Author: Romain Brenguier

regression/strings/Makefile

@@ -1,3 +1,6 @@
 
 test:
-	../test.pl -c ../../../src/cbmc/cbmc
+	@../test.pl -c ../../../src/cbmc/cbmc
+
+testfuture:
+	@../test.pl -c ../../../src/cbmc/cbmc -F

regression/strings/cprover-string-hack.h

@@ -56,7 +56,7 @@ typedef unsigned char __CPROVER_char;
  ******************************************************************************/
 extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2);
-extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func();
+extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func(char * str);
 extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func();
 extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2);
 extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str);
@@ -68,5 +68,5 @@ extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __
 extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
-extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
-extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i);
+extern int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
+extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int i);

regression/strings/java_case/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_case.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$

regression/strings/java_char_array/test.desc

@@ -0,0 +1,9 @@
+FUTURE
+test_char_array.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_char_array.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_char_array.java line 12: SUCCESS$
+^\[assertion.3\] assertion at file test_char_array.java line 13: FAILURE$
+--

regression/strings/java_char_array/test_char_array.class

@@ -0,0 +1,15 @@
+public class test_char_array {
+
+    public static void main(String[] argv)
+    {
+        String s = "abc";
+        char [] str = s.toCharArray();
+        int[] test = new int[312];
+        char c = str[2];
+        String t = argv[0];
+        char d = t.charAt(0);
+        assert(str.length == 3);
+        assert(c == 'c');
+        assert(c == d || d < 'a' || d > 'z' );
+    }
+}

regression/strings/java_char_array/test_char_array.java

@@ -0,0 +1,11 @@
+FUTURE
+test_init.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_init.java line 16: SUCCESS$
+^\[assertion.2\] assertion at file test_init.java line 17: SUCCESS$
+^\[assertion.3\] assertion at file test_init.java line 18: SUCCESS$
+^\[assertion.4\] assertion at file test_init.java line 20: SUCCESS$
+^\[assertion.5\] assertion at file test_init.java line 21: FAILURE$
+--

regression/strings/java_char_array_init/test.desc

@@ -0,0 +1,23 @@
+public class test_init {
+
+    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);
+
+	System.out.println(s);
+	System.out.println(s.length());
+	assert(s.startsWith("Hello"));
+	assert(s.length() == 10);
+	assert(t.equals("el"));
+	String u = String.valueOf(str,3,2);
+	assert(u.equals("lo"));
+	assert(s.equals("Hello") || !t.equals("el") || !u.equals("lo"));
+    }
+}

regression/strings/java_char_array_init/test_init.class

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_char_at.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$

regression/strings/java_char_array_init/test_init.java

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_code_point.class
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$

regression/strings/java_char_at/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_compare.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$

regression/strings/java_code_point/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_concat.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$

regression/strings/java_compare/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test_contains.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$

regression/strings/java_concat/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test_delete.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$

regression/strings/java_contains/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 easychair.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$

regression/strings/java_delete/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_empty.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$

regression/strings/java_easychair/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_equal.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$

regression/strings/java_empty/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_float.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$

regression/strings/java_equal/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_index_of.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$

regression/strings/java_float/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_int.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$

regression/strings/java_index_of/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_prefix.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$

regression/strings/java_int/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_replace.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$

regression/strings/java_prefix/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_set_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$

regression/strings/java_replace/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_string_builder.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$

regression/strings/java_set_length/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_insert.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_insert.java line 17: SUCCESS$
+^\[assertion.2\] assertion at file test_insert.java line 18: FAILURE$
+--

regression/strings/java_string_builder/test.desc

@@ -0,0 +1,20 @@
+public class test_insert {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[5];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+
+
+	StringBuilder sb = new StringBuilder(" world");
+	sb.insert(0,str);
+	String s = sb.toString();
+	System.out.println(s);
+	assert(s.equals("Hello world"));
+	assert(!s.equals("Hello world"));
+    }
+}

regression/strings/java_string_builder_insert/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_sb_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 \[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$

regression/strings/java_string_builder_insert/test_insert.class

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$

regression/strings/java_string_builder_insert/test_insert.java

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_substring.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$

regression/strings/java_string_builder_length/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_suffix.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$

regression/strings/java_strlen/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_trim.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$

regression/strings/java_substring/test.desc

@@ -5,13 +5,13 @@
 int main()
 {
     __CPROVER_string s;
-    __CPROVER_char c1, c2;
+    char c1, c2;
     int i;
     int j;
     i = 2;
     s = __CPROVER_string_literal("pippo");
     c1 = __CPROVER_char_at(s, i);
-    c2 = __CPROVER_char_literal("p");
+    c2 = 'p';
     assert (c1 == c2);
     assert (c1 != c2);
     return 0;

regression/strings/java_suffix/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion c1 == c2: SUCCESS$

regression/strings/java_trim/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion n == 5: SUCCESS$

regression/strings/test1/test.c

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings/test1/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings/test2/test.desc

@@ -16,7 +16,7 @@ int main()
     // proving the assertions individually seems to be much faster
     //assert(__CPROVER_string_length(s) == i + 5);
     //assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s));
-    assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
+    assert(__CPROVER_char_at(s, i) == 'p');
 
     return 0;
 }

regression/strings/test3.1/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings/test3.2/test.desc

@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$