Regressions tests for string functions

regression/strings/Makefile

@@ -0,0 +1,3 @@
+
+test:
+	../test.pl -c ../../../src/cbmc/cbmc

regression/strings/cprover-string-hack.h

@@ -0,0 +1,73 @@
+typedef struct __CPROVER_string { char *s; } __CPROVER_string;
+//typedef struct __CPROVER_char { char c; } __CPROVER_char;
+typedef unsigned char __CPROVER_char;
+
+/******************************************************************************
+ * CPROVER string functions
+ ******************************************************************************/
+/* returns s[p] */
+#define __CPROVER_char_at(s, p) __CPROVER_uninterpreted_string_char_at_func(s, p)
+
+/* string equality */
+#define __CPROVER_string_equal(s1, s2) __CPROVER_uninterpreted_string_equal_func(s1, s2)
+
+/* defines a string literal, e.g. __CPROVER_string_literal("foo") */
+#define __CPROVER_string_literal(s) __CPROVER_uninterpreted_string_literal_func(s)
+
+/* defines a char literal, e.g. __CPROVER_char_literal("c"). NOTE: you
+ * *must* use a C string literal as argument (i.e. double quotes "c", not
+ * single 'c') */
+#define __CPROVER_char_literal(c) __CPROVER_uninterpreted_char_literal_func(c)
+
+/* produces the concatenation of s1 and s2 */
+#define __CPROVER_string_concat(s1, s2) __CPROVER_uninterpreted_string_concat_func(s1, s2)
+
+/* return the length of s */
+#define __CPROVER_string_length(s) __CPROVER_uninterpreted_string_length_func(s)
+
+/* extracts the substring between positions i and j (j not included) */
+#define __CPROVER_string_substring(s, i, j) __CPROVER_uninterpreted_string_substring_func(s, i, j)
+
+/* test whether p is a prefix of s */
+#define __CPROVER_string_isprefix(p, s) __CPROVER_uninterpreted_string_is_prefix_func(p, s)
+
+/* test whether p is a suffix of s */
+#define __CPROVER_string_issuffix(p, s) __CPROVER_uninterpreted_string_is_suffix_func(p, s)
+/* test whether p contains s */
+#define __CPROVER_string_contains(p, s) __CPROVER_uninterpreted_string_contains_func(p, s)
+
+/* first index where character c appears, -1 if not found */
+#define __CPROVER_string_index_of(s, c) __CPROVER_uninterpreted_string_index_of_func(s, c)
+
+/* last index where character c appears */
+#define __CPROVER_string_last_index_of(s, c) __CPROVER_uninterpreted_string_last_index_of_func(s, c)
+
+/* returns a new string obtained from s by setting s[p] = c */
+#define __CPROVER_char_set(s, p, c) __CPROVER_uninterpreted_string_char_set_func(s, p, c)
+
+
+#define __CPROVER_string_copy(s) __CPROVER_uninterpreted_string_copy_func(s)
+#define __CPROVER_parse_int(s) __CPROVER_uninterpreted_string_parse_int_func(s)
+#define __CPROVER_string_of_int(i) __CPROVER_uninterpreted_string_of_int_func(i)
+
+
+/******************************************************************************
+ * don't use these directly
+ ******************************************************************************/
+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_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);
+extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j);
+extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str);
+extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str);
+extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2);
+extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c);
+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);
+

regression/strings/java_case/test.desc

@@ -0,0 +1,10 @@
+CORE
+test_case.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_case.java line 12: SUCCESS$
+^\[assertion.3\] assertion at file test_case.java line 13: SUCCESS$
+^\[assertion.4\] assertion at file test_case.java line 14: FAILURE$
+--

regression/strings/java_case/test_case.java

@@ -0,0 +1,16 @@
+public class test_case {
+
+    public static void main(String[] argv) {
+
+	String s = new String("AbcCdE");
+	String l = s.toLowerCase();
+	System.out.println(l);
+
+	String u = s.toUpperCase();
+	System.out.println(u);
+	assert(l.equals("abccde"));
+	assert(u.equals("ABCCDE"));
+	assert(s.equalsIgnoreCase("ABccDe"));
+	assert(!l.equals("abccde") || !u.equals("ABCCDE"));
+    }
+}

regression/strings/java_char_at/test.desc

@@ -0,0 +1,9 @@
+CORE
+test_char_at.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_char_at.java line 13: FAILURE$
+^\[assertion.3\] assertion at file test_char_at.java line 15: SUCCESS$
+--

regression/strings/java_char_at/test_char_at.java

@@ -0,0 +1,17 @@
+public class test_char_at {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	char c = s.charAt(4);
+	StringBuilder sb = new StringBuilder(s);
+	sb.setCharAt(5,'-');
+	s = sb.toString();
+
+	if(argv.length==1)
+	    assert(c == 'o');
+	else if(argv.length==2)
+	    assert(c == 'p');
+	else
+	    assert(s.equals("Hello-World!"));
+    }
+}

regression/strings/java_code_point/test.desc

@@ -0,0 +1,11 @@
+CORE
+test_code_point.class
+--pass
+^EXIT=0$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$
+^\[assertion.2\] assertion at file test_code_point.java line 6: SUCCESS$
+^\[assertion.3\] assertion at file test_code_point.java line 7: SUCCESS$
+^\[assertion.4\] assertion at file test_code_point.java line 8: SUCCESS$
+^\[assertion.5\] assertion at file test_code_point.java line 11: SUCCESS$
+--

regression/strings/java_code_point/test_code_point.java

@@ -0,0 +1,13 @@
+public class test_code_point {
+
+    public static void main(String[] argv) {
+	String s = "!𐤇𐤄𐤋𐤋𐤅"; 
+	assert(s.codePointAt(1) == 67847);
+	assert(s.codePointBefore(3) == 67847);
+	assert(s.codePointCount(1,5) >= 2);
+	assert(s.offsetByCodePoints(1,2) >= 3);
+	StringBuilder sb = new StringBuilder();
+	sb.appendCodePoint(0x10907);
+	assert(s.charAt(1) == sb.charAt(0));
+    }
+}

regression/strings/java_compare/test.desc

@@ -0,0 +1,10 @@
+CORE
+test_compare.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$
+^\[assertion.2\] assertion at file test_compare.java line 8: FAILURE$
+^\[assertion.3\] assertion at file test_compare.java line 11: SUCCESS$
+^\[assertion.4\] assertion at file test_compare.java line 12: FAILURE$
+--

regression/strings/java_compare/test_compare.java

@@ -0,0 +1,18 @@
+public class test_compare {
+
+    public static void main(String[] argv) {
+	String s1 = "abc";
+	String s2 = "aac";
+	assert(s1.compareTo(s2) == 1);
+
+	assert(s2.compareTo(argv[0]) != -1);
+
+	String s3 = "abc";
+	assert(s3.hashCode() == s1.hashCode());
+	assert(s3.hashCode() == s2.hashCode());
+
+	/*String x = s1.intern();
+	String y = s3.intern();
+	assert(x == y);*/
+    }
+}

regression/strings/java_concat/test.desc

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

regression/strings/java_concat/test_concat.java

@@ -0,0 +1,12 @@
+public class test_concat {
+
+    public static void main(String[] argv) {
+	String s = new String("pi");
+	int i = s.length();
+	String t = new String("ppo");
+	String u = s.concat(t);
+	char c = u.charAt(i);
+	assert(c == 'p');
+	assert(c == 'o');
+    }
+}

regression/strings/java_contains/test.desc

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

regression/strings/java_contains/test_contains.java

@@ -0,0 +1,10 @@
+public class test_contains {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	String u = "o W";
+	String t = "W o";
+	assert(s.contains(u));	
+	assert(s.contains(t));
+    }
+}

regression/strings/java_delete/test.desc

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

regression/strings/java_delete/test_delete.java

@@ -0,0 +1,15 @@
+public class test_delete {
+
+    public static void main(String[] argv) {
+	StringBuilder s = new StringBuilder();
+	s.append("Hello World!");
+	s.delete(4,6);
+	s.deleteCharAt(1);
+
+	String str = s.toString();
+	System.out.println(str);
+	assert(str.equals("HllWorld!"));
+	assert(!str.equals("HllWorld!"));
+
+    }
+}

regression/strings/java_easychair/easychair.java

@@ -0,0 +1,34 @@
+public class easychair {
+
+    public static void main(String[] argv) {
+	if(argv.length > 1){
+	    String str = new String(argv[1]);
+	    if(str.length() < 40){
+
+		// containing "/" and containing "EasyChair"
+		int lastSlash = str.lastIndexOf('/');
+		if(lastSlash < 0) return ;
+
+		String rest = str.substring(lastSlash + 1);
+		// warning: removed this because contains is not efficient at the moment
+		if(! rest.contains("EasyChair")) return ;
+		// (2) Check that str starts with "http://"
+		if(! str.startsWith("http://")) return ;
+		// (3) Take the string between "http://" and the last "/".
+		// if it starts with "www." strip the "www." off
+		String t = str.substring("http://".length(),lastSlash - "http://".length());
+		if(t.startsWith("www."))
+		    t = t.substring("www.".length());
+
+		//
+		//(4) Check that after stripping we have either "live.com"
+		// or "google.com"
+		if(!t.equals("live.com") && !t.equals("google.com"))
+		    return ;
+		// s survived all checks
+		assert(false); //return true;
+	    }
+	}
+    }
+
+}

regression/strings/java_easychair/test.desc

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

regression/strings/java_empty/test.desc

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

regression/strings/java_empty/test_empty.java

@@ -0,0 +1,7 @@
+public class test_empty {
+    public static void main(String[] argv) {
+	String empty = "   ";
+	assert(empty.trim().isEmpty());
+	assert(empty.isEmpty());
+    }
+}

regression/strings/java_equal/test.desc

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

regression/strings/java_equal/test_equal.java

@@ -0,0 +1,10 @@
+public class test_equal {
+
+    public static void main(String[] argv) {
+	String s = new String("pi");
+	String t = new String("po");
+	String u = "po";
+	assert(s.equals(t));
+	assert(t.equals(u));
+    }
+}

regression/strings/java_float/test.desc

@@ -0,0 +1,10 @@
+CORE
+test_float.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$
+^\[assertion.2\] assertion at file test_float.java line 15: SUCCESS$
+^\[assertion.3\] assertion at file test_float.java line 16: SUCCESS$
+^\[assertion.4\] assertion at file test_float.java line 17: FAILURE$
+--

regression/strings/java_float/test_float.java

@@ -0,0 +1,20 @@
+public class test_float {
+
+    public static void main(String[] arg) {
+	float inf = 100.0f / 0.0f;
+	float minus_inf = -100.0f / 0.0f;
+	float nan = 0.0f / 0.0f;
+	String inf_string = Float.toString(inf);
+	String mininf_string = Float.toString(minus_inf);
+	String nan_string = Float.toString(nan);
+	//String arg1 = arg[0];
+	System.out.println(nan_string);
+	System.out.println(inf_string);
+	System.out.println(mininf_string);
+	assert(nan_string.equals("NaN"));
+	assert(inf_string.equals("Infinity"));
+	assert(mininf_string.equals("-Infinity"));
+	assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity")
+	       || !mininf_string.equals("-Infinity"));
+    }
+}

regression/strings/java_index_of/test.desc

@@ -0,0 +1,16 @@
+CORE
+test_index_of.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$
+^\[assertion.2\] assertion at file test_index_of.java line 14: FAILURE$
+^\[assertion.3\] assertion at file test_index_of.java line 17: SUCCESS$
+^\[assertion.4\] assertion at file test_index_of.java line 18: FAILURE$
+^\[assertion.5\] assertion at file test_index_of.java line 21: SUCCESS$
+^\[assertion.6\] assertion at file test_index_of.java line 22: FAILURE$
+^\[assertion.7\] assertion at file test_index_of.java line 25: SUCCESS$
+^\[assertion.8\] assertion at file test_index_of.java line 26: FAILURE$
+^\[assertion.9\] assertion at file test_index_of.java line 28: SUCCESS$
+^\[assertion.10\] assertion at file test_index_of.java line 29: SUCCESS$
+--