String solver

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,6 @@ 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
 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 @@
+CORE
+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.java

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

@@ -0,0 +1,11 @@
+CORE
+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_init.java

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

@@ -1,6 +1,6 @@
 CORE
 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_code_point/test.desc

@@ -1,6 +1,6 @@
 CORE
 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_compare/test.desc

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

regression/strings/java_concat/test.desc

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

regression/strings/java_contains/test.desc

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

regression/strings/java_delete/test.desc

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

regression/strings/java_easychair/test.desc

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

regression/strings/java_empty/test.desc

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

regression/strings/java_equal/test.desc

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

regression/strings/java_float/test.desc

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

regression/strings/java_index_of/test.desc

@@ -1,6 +1,6 @@
 CORE
 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_int/test.desc

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

regression/strings/java_prefix/test.desc

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

regression/strings/java_replace/test.desc

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

regression/strings/java_set_length/test.desc

@@ -1,6 +1,6 @@
 CORE
 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_string_builder/test.desc

@@ -1,6 +1,6 @@
 CORE
 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_string_builder_insert/test.desc

@@ -0,0 +1,8 @@
+CORE
+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_insert/test_insert.java

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

@@ -1,6 +1,6 @@
 CORE
 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_strlen/test.desc

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

regression/strings/java_substring/test.desc

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

regression/strings/java_suffix/test.desc

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

regression/strings/java_trim/test.desc

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

regression/strings/test1/test.c

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

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

regression/strings/test2/test.desc

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

regression/strings/test3.1/test.desc

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

regression/strings/test3.2/test.desc

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

regression/strings/test3.3/test.c

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

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

regression/strings/test3.4/test.desc

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

regression/strings/test3/test.c

@@ -14,7 +14,7 @@ int main()
 
     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');
     assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s));
 
     return 0;

regression/strings/test3/test.desc

@@ -1,10 +1,10 @@
 CORE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s) == i + 5: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.3\] assertion __CPROVER_uninterpreted_string_char_at_func(s, i) == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.4\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"p!o\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s) == i + 5: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$
+^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == .p.: SUCCESS$
+^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"p!o\"), s): FAILURE$
 --

regression/strings/test4/test.c

@@ -9,7 +9,7 @@ int main()
     int j;
     i = 2;
     s = __CPROVER_string_literal("pippo");
-    if (__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")) {
+    if (__CPROVER_char_at(s, i) == 'p') {
         j = 1;
     }
     assert(j == 1);