Skip to content

Commit a1b6623

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#272 from romainbrenguier/string-solver-regressions
Regressions tests for string functions
2 parents 7182882 + e6d97e1 commit a1b6623

File tree

119 files changed

+1367
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

119 files changed

+1367
-0
lines changed

‎regression/strings/Makefile

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
2+
test:
3+
../test.pl -c ../../../src/cbmc/cbmc

‎regression/strings/cprover-string-hack.h

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
typedef struct __CPROVER_string { char *s; } __CPROVER_string;
2+
//typedef struct __CPROVER_char { char c; } __CPROVER_char;
3+
typedef unsigned char __CPROVER_char;
4+
5+
/******************************************************************************
6+
* CPROVER string functions
7+
******************************************************************************/
8+
/* returns s[p] */
9+
#define __CPROVER_char_at(s, p) __CPROVER_uninterpreted_string_char_at_func(s, p)
10+
11+
/* string equality */
12+
#define __CPROVER_string_equal(s1, s2) __CPROVER_uninterpreted_string_equal_func(s1, s2)
13+
14+
/* defines a string literal, e.g. __CPROVER_string_literal("foo") */
15+
#define __CPROVER_string_literal(s) __CPROVER_uninterpreted_string_literal_func(s)
16+
17+
/* defines a char literal, e.g. __CPROVER_char_literal("c"). NOTE: you
18+
* *must* use a C string literal as argument (i.e. double quotes "c", not
19+
* single 'c') */
20+
#define __CPROVER_char_literal(c) __CPROVER_uninterpreted_char_literal_func(c)
21+
22+
/* produces the concatenation of s1 and s2 */
23+
#define __CPROVER_string_concat(s1, s2) __CPROVER_uninterpreted_string_concat_func(s1, s2)
24+
25+
/* return the length of s */
26+
#define __CPROVER_string_length(s) __CPROVER_uninterpreted_string_length_func(s)
27+
28+
/* extracts the substring between positions i and j (j not included) */
29+
#define __CPROVER_string_substring(s, i, j) __CPROVER_uninterpreted_string_substring_func(s, i, j)
30+
31+
/* test whether p is a prefix of s */
32+
#define __CPROVER_string_isprefix(p, s) __CPROVER_uninterpreted_string_is_prefix_func(p, s)
33+
34+
/* test whether p is a suffix of s */
35+
#define __CPROVER_string_issuffix(p, s) __CPROVER_uninterpreted_string_is_suffix_func(p, s)
36+
/* test whether p contains s */
37+
#define __CPROVER_string_contains(p, s) __CPROVER_uninterpreted_string_contains_func(p, s)
38+
39+
/* first index where character c appears, -1 if not found */
40+
#define __CPROVER_string_index_of(s, c) __CPROVER_uninterpreted_string_index_of_func(s, c)
41+
42+
/* last index where character c appears */
43+
#define __CPROVER_string_last_index_of(s, c) __CPROVER_uninterpreted_string_last_index_of_func(s, c)
44+
45+
/* returns a new string obtained from s by setting s[p] = c */
46+
#define __CPROVER_char_set(s, p, c) __CPROVER_uninterpreted_string_char_set_func(s, p, c)
47+
48+
49+
#define __CPROVER_string_copy(s) __CPROVER_uninterpreted_string_copy_func(s)
50+
#define __CPROVER_parse_int(s) __CPROVER_uninterpreted_string_parse_int_func(s)
51+
#define __CPROVER_string_of_int(i) __CPROVER_uninterpreted_string_of_int_func(i)
52+
53+
54+
/******************************************************************************
55+
* don't use these directly
56+
******************************************************************************/
57+
extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
58+
extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2);
59+
extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func();
60+
extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func();
61+
extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2);
62+
extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str);
63+
extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j);
64+
extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str);
65+
extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str);
66+
extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2);
67+
extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c);
68+
extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
69+
extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
70+
extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
71+
extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
72+
extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i);
73+

‎regression/strings/java_case/test.desc

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

‎regression/strings/java_case/test_case.class

1.05 KB
Binary file not shown.

‎regression/strings/java_case/test_case.java

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
public class test_case {
2+
3+
public static void main(String[] argv) {
4+
5+
String s = new String("AbcCdE");
6+
String l = s.toLowerCase();
7+
System.out.println(l);
8+
9+
String u = s.toUpperCase();
10+
System.out.println(u);
11+
assert(l.equals("abccde"));
12+
assert(u.equals("ABCCDE"));
13+
assert(s.equalsIgnoreCase("ABccDe"));
14+
assert(!l.equals("abccde") || !u.equals("ABCCDE"));
15+
}
16+
}

‎regression/strings/java_char_at/test.desc

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

‎regression/strings/java_char_at/test_char_at.class

951 Bytes
Binary file not shown.

‎regression/strings/java_char_at/test_char_at.java

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
public class test_char_at {
2+
3+
public static void main(String[] argv) {
4+
String s = new String("Hello World!");
5+
char c = s.charAt(4);
6+
StringBuilder sb = new StringBuilder(s);
7+
sb.setCharAt(5,'-');
8+
s = sb.toString();
9+
10+
if(argv.length==1)
11+
assert(c == 'o');
12+
else if(argv.length==2)
13+
assert(c == 'p');
14+
else
15+
assert(s.equals("Hello-World!"));
16+
}
17+
}

‎regression/strings/java_code_point/test.desc

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

‎regression/strings/java_code_point/test_code_point.class

1 KB
Binary file not shown.

‎regression/strings/java_code_point/test_code_point.java

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
public class test_code_point {
2+
3+
public static void main(String[] argv) {
4+
String s = "!𐤇𐤄𐤋𐤋𐤅";
5+
assert(s.codePointAt(1) == 67847);
6+
assert(s.codePointBefore(3) == 67847);
7+
assert(s.codePointCount(1,5) >= 2);
8+
assert(s.offsetByCodePoints(1,2) >= 3);
9+
StringBuilder sb = new StringBuilder();
10+
sb.appendCodePoint(0x10907);
11+
assert(s.charAt(1) == sb.charAt(0));
12+
}
13+
}

‎regression/strings/java_compare/test.desc

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

‎regression/strings/java_compare/test_compare.class

780 Bytes
Binary file not shown.

‎regression/strings/java_compare/test_compare.java

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
public class test_compare {
2+
3+
public static void main(String[] argv) {
4+
String s1 = "abc";
5+
String s2 = "aac";
6+
assert(s1.compareTo(s2) == 1);
7+
8+
assert(s2.compareTo(argv[0]) != -1);
9+
10+
String s3 = "abc";
11+
assert(s3.hashCode() == s1.hashCode());
12+
assert(s3.hashCode() == s2.hashCode());
13+
14+
/*String x = s1.intern();
15+
String y = s3.intern();
16+
assert(x == y);*/
17+
}
18+
}

‎regression/strings/java_concat/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test_concat.class
3+
--pass
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$
7+
^\[assertion.2\] assertion at file test_concat.java line 10: FAILURE$
8+
--

‎regression/strings/java_concat/test_concat.class

854 Bytes
Binary file not shown.

‎regression/strings/java_concat/test_concat.java

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
public class test_concat {
2+
3+
public static void main(String[] argv) {
4+
String s = new String("pi");
5+
int i = s.length();
6+
String t = new String("ppo");
7+
String u = s.concat(t);
8+
char c = u.charAt(i);
9+
assert(c == 'p');
10+
assert(c == 'o');
11+
}
12+
}

‎regression/strings/java_contains/test.desc

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

‎regression/strings/java_contains/test_contains.class

753 Bytes
Binary file not shown.

‎regression/strings/java_contains/test_contains.java

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
public class test_contains {
2+
3+
public static void main(String[] argv) {
4+
String s = new String("Hello World!");
5+
String u = "o W";
6+
String t = "W o";
7+
assert(s.contains(u));
8+
assert(s.contains(t));
9+
}
10+
}

‎regression/strings/java_delete/test.desc

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

‎regression/strings/java_delete/test_delete.class

1.1 KB
Binary file not shown.

‎regression/strings/java_delete/test_delete.java

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
public class test_delete {
2+
3+
public static void main(String[] argv) {
4+
StringBuilder s = new StringBuilder();
5+
s.append("Hello World!");
6+
s.delete(4,6);
7+
s.deleteCharAt(1);
8+
9+
String str = s.toString();
10+
System.out.println(str);
11+
assert(str.equals("HllWorld!"));
12+
assert(!str.equals("HllWorld!"));
13+
14+
}
15+
}

‎regression/strings/java_easychair/easychair.class

1.14 KB
Binary file not shown.

‎regression/strings/java_easychair/easychair.java

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
public class easychair {
2+
3+
public static void main(String[] argv) {
4+
if(argv.length > 1){
5+
String str = new String(argv[1]);
6+
if(str.length() < 40){
7+
8+
// containing "/" and containing "EasyChair"
9+
int lastSlash = str.lastIndexOf('/');
10+
if(lastSlash < 0) return ;
11+
12+
String rest = str.substring(lastSlash + 1);
13+
// warning: removed this because contains is not efficient at the moment
14+
if(! rest.contains("EasyChair")) return ;
15+
// (2) Check that str starts with "http://"
16+
if(! str.startsWith("http://")) return ;
17+
// (3) Take the string between "http://" and the last "/".
18+
// if it starts with "www." strip the "www." off
19+
String t = str.substring("http://".length(),lastSlash - "http://".length());
20+
if(t.startsWith("www."))
21+
t = t.substring("www.".length());
22+
23+
//
24+
//(4) Check that after stripping we have either "live.com"
25+
// or "google.com"
26+
if(!t.equals("live.com") && !t.equals("google.com"))
27+
return ;
28+
// s survived all checks
29+
assert(false); //return true;
30+
}
31+
}
32+
}
33+
34+
}

‎regression/strings/java_easychair/test.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
easychair.class
3+
--pass
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$
7+
--

‎regression/strings/java_empty/test.desc

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

‎regression/strings/java_empty/test_empty.class

669 Bytes
Binary file not shown.

‎regression/strings/java_empty/test_empty.java

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
public class test_empty {
2+
public static void main(String[] argv) {
3+
String empty = " ";
4+
assert(empty.trim().isEmpty());
5+
assert(empty.isEmpty());
6+
}
7+
}

‎regression/strings/java_equal/test.desc

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

‎regression/strings/java_equal/test_equal.class

726 Bytes
Binary file not shown.

‎regression/strings/java_equal/test_equal.java

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
public class test_equal {
2+
3+
public static void main(String[] argv) {
4+
String s = new String("pi");
5+
String t = new String("po");
6+
String u = "po";
7+
assert(s.equals(t));
8+
assert(t.equals(u));
9+
}
10+
}

‎regression/strings/java_float/test.desc

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

‎regression/strings/java_float/test_float.class

1.07 KB
Binary file not shown.

‎regression/strings/java_float/test_float.java

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
public class test_float {
2+
3+
public static void main(String[] arg) {
4+
float inf = 100.0f / 0.0f;
5+
float minus_inf = -100.0f / 0.0f;
6+
float nan = 0.0f / 0.0f;
7+
String inf_string = Float.toString(inf);
8+
String mininf_string = Float.toString(minus_inf);
9+
String nan_string = Float.toString(nan);
10+
//String arg1 = arg[0];
11+
System.out.println(nan_string);
12+
System.out.println(inf_string);
13+
System.out.println(mininf_string);
14+
assert(nan_string.equals("NaN"));
15+
assert(inf_string.equals("Infinity"));
16+
assert(mininf_string.equals("-Infinity"));
17+
assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity")
18+
|| !mininf_string.equals("-Infinity"));
19+
}
20+
}

‎regression/strings/java_index_of/test.desc

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

‎regression/strings/java_index_of/test_index_of.class

1.08 KB
Binary file not shown.

0 commit comments

Comments
 (0)