Skip to content

Commit faf8f00

Browse files
smowtonsmowton
committed
Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104
2 parents 5266ba2 + 67ec6f2 commit faf8f00

File tree

104 files changed

+2257
-1083
lines changed

Some content is hidden

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

104 files changed

+2257
-1083
lines changed

‎regression/jbmc-strings/StaticCharMethods05/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ StaticCharMethods05.class
33
--refine-strings --string-max-length 1000
44
^EXIT=10$
55
^SIGNAL=0$
6-
null-pointer-exception\.14\] Throw null: FAILURE
76
^\[.*assertion\.1\] .* line 12 .* FAILURE$
87
^\[.*assertion\.2\] .* line 22 .* FAILURE$
98
^VERIFICATION FAILED$

‎regression/jbmc-strings/StringIndexOf/Test.class

1.15 KB
Binary file not shown.

‎regression/jbmc-strings/StringIndexOf/Test.java

+46
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
public class Test {
2+
3+
public boolean check(String input_String, char input_char, int input_int) {
4+
// Verify indexOf is conform to its specification
5+
int i = input_String.indexOf(input_char, input_int);
6+
7+
assert i < input_String.length();
8+
9+
int lower_bound;
10+
if (input_int < 0)
11+
lower_bound = 0;
12+
else
13+
lower_bound = input_int;
14+
15+
if (i == -1) {
16+
for (int j = lower_bound; j < input_String.length(); j++)
17+
assert input_String.charAt(j) != input_char;
18+
} else {
19+
assert i >= lower_bound;
20+
assert input_String.charAt(i) == input_char;
21+
22+
for (int j = lower_bound; j < i; j++)
23+
assert input_String.charAt(j) != input_char;
24+
}
25+
return true;
26+
}
27+
28+
public boolean check2() {
29+
// Verification should fail, this is to check the solver does
30+
// not get a contradiction
31+
int i = "hello".indexOf('o', 1);
32+
assert i == 4;
33+
i = "hello".indexOf('h', 1);
34+
assert i == -1;
35+
i = "hello".indexOf('e', 4);
36+
assert i == -1;
37+
i = "hello".indexOf('e', 8);
38+
assert i == -1;
39+
i = "hello".indexOf('x', 0);
40+
assert i == -1;
41+
i = "hello".indexOf('h', -1000);
42+
assert i == 0;
43+
assert false;
44+
return true;
45+
}
46+
}

‎regression/jbmc-strings/StringIndexOf/test.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
Test.class
3+
--refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--

‎regression/jbmc-strings/StringIndexOf/test2.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
Test.class
3+
--refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
assertion at file Test.java line 32 .* SUCCESS
7+
assertion at file Test.java line 34 .* SUCCESS
8+
assertion at file Test.java line 36 .* SUCCESS
9+
assertion at file Test.java line 38 .* SUCCESS
10+
assertion at file Test.java line 40 .* SUCCESS
11+
assertion at file Test.java line 42 .* SUCCESS
12+
assertion at file Test.java line 43 .* FAILURE
13+
^VERIFICATION FAILED$
14+
--

‎regression/jbmc-strings/StringIndexOf/test_thorough.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
THOROUGH
2+
Test.class
3+
--refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--

‎regression/jbmc-strings/StringLastIndexOf/Test.class

49 Bytes
Binary file not shown.

‎regression/jbmc-strings/StringLastIndexOf/Test.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ public void check(String input_String1, String input_String2, int i) {
1313
// Contradiction with the previous condition (should fail).
1414
assert "foo".lastIndexOf("") != 3;
1515
} else if (i == 2 && input_String2.length() > 0) {
16-
int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
16+
int lio = input_String1.lastIndexOf(org.cprover.CProverString.charAt(input_String2, 0), fromIndex);
1717
if (input_String2.length() == 0)
1818
assert lio == fromIndex;
1919
} else if (i == 3) {

‎regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class

49 Bytes
Binary file not shown.

‎regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -8,19 +8,19 @@ public static char[] toCharArray(String s)
88
char arr[]=new char[s.length()];
99
// We limit arbitrarly the loop unfolding to 10
1010
for(int i=0; i<length && i<10; i++)
11-
arr[i]=s.charAt(i);
11+
arr[i]=org.cprover.CProverString.charAt(s, i);
1212
return arr;
1313
}
1414

1515
public static void main(String[] args)
1616
{
1717
String s1 = "diffblue";
1818
String s2 = "TESTGENERATION";
19-
String s3 = " automated ";
19+
String s3 = " automated ";
2020

2121
assert s1.equals("diffblue");
2222
assert s2.equals("TESTGENERATION");
23-
assert s3.equals(" automated ");
23+
assert s3.equals(" automated ");
2424

2525
System.out.printf(
2626
"Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
@@ -43,7 +43,7 @@ public static void main(String[] args)
4343
int i=0;
4444
for (char character : charArray)
4545
{
46-
assert character=="diffblue".charAt(i);
46+
assert character==org.cprover.CProverString.charAt("diffblue", i);
4747
++i;
4848
}
4949

‎regression/jbmc-strings/SubString01/SubString01.class

67 Bytes
Binary file not shown.

‎regression/jbmc-strings/SubString01/SubString01.java

+8-9
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,12 @@
11
public class SubString01
22
{
3-
public static void main(String[] args)
4-
{
5-
String letters = "automatictestcasegenerationatdiffblue";
3+
public static void main(String[] args)
4+
{
5+
String letters = "automatictestcasegenerationatdiffblue";
66

7-
String tmp=letters.substring(20);
8-
assert tmp.equals("erationatdiffblue");
9-
10-
tmp=letters.substring(9, 13);
11-
assert tmp.equals("test");
12-
}
7+
String tmp=org.cprover.CProverString.substring(letters, 20);
8+
assert tmp.equals("erationatdiffblue");
9+
tmp=org.cprover.CProverString.substring(letters, 9, 13);
10+
assert tmp.equals("test");
11+
}
1312
}

‎regression/jbmc-strings/cprover/CProverString.class

790 Bytes
Binary file not shown.

‎regression/jbmc-strings/cprover/CProverString.java

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package org.cprover;
2+
3+
public final class CProverString {
4+
public static char charAt(String s, int i) {
5+
if (0 <= i && i < s.length())
6+
return s.charAt(i);
7+
else
8+
return '\u0000';
9+
}
10+
11+
public static String substring(String s, int i) {
12+
if (i <= 0)
13+
return s;
14+
else if (i >= s.length())
15+
return "";
16+
else
17+
return s.substring(i);
18+
}
19+
20+
public static String substring(String s, int i, int j) {
21+
if (i < 0)
22+
return substring(s, 0, j);
23+
if (j >= s.length())
24+
return substring(s, 0, s.length() - 1);
25+
if (i >= j)
26+
return "";
27+
return s.substring(i, j);
28+
}
29+
}

‎regression/jbmc-strings/java_char_array_init/test_init.class

49 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_char_array_init/test_init.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ public static String stringOfCharArray(char arr[])
1313

1414
public static String stringOfCharArray(char arr[], int i, int j)
1515
{
16-
return stringOfCharArray(arr).substring(i, i+j);
16+
return org.cprover.CProverString.substring(stringOfCharArray(arr), i, i+j);
1717
}
1818

1919
public static void main(int i)

‎regression/jbmc-strings/java_concat/test_concat.class

49 Bytes
Binary file not shown.

‎regression/jbmc-strings/java_concat/test_concat.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
66
int i = s.length();
77
String t = new String("ppo");
88
String u = s.concat(t);
9-
char c = u.charAt(i);
9+
char c = org.cprover.CProverString.charAt(u, i);
1010
assert(c == 'p');
1111
assert(c != 'p');
1212
}

‎regression/strings-smoke-tests/cprover/CProverString.class

790 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/cprover/CProverString.java

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package org.cprover;
2+
3+
public final class CProverString {
4+
public static char charAt(String s, int i) {
5+
if (0 <= i && i < s.length())
6+
return s.charAt(i);
7+
else
8+
return '\u0000';
9+
}
10+
11+
public static String substring(String s, int i) {
12+
if (i <= 0)
13+
return s;
14+
else if (i >= s.length())
15+
return "";
16+
else
17+
return s.substring(i);
18+
}
19+
20+
public static String substring(String s, int i, int j) {
21+
if (i < 0)
22+
return substring(s, 0, j);
23+
if (j >= s.length())
24+
return substring(s, 0, s.length() - 1);
25+
if (i >= j)
26+
return "";
27+
return s.substring(i, j);
28+
}
29+
}

‎regression/strings-smoke-tests/java_append_string/test_append_string.class

49 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_append_string/test_append_string.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ public static void check(StringBuilder sb, String str)
2020
sb.append(str, 2, 4);
2121
String res = sb.toString();
2222
assert(res.startsWith(init));
23-
assert(res.endsWith(str.substring(2, 4)));
23+
assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));
2424
assert(res.length() == init.length() + 2);
2525
assert(!res.equals("foobarfuz"));
2626
}

‎regression/strings-smoke-tests/java_char_array/test_char_array.class

49 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_char_array/test_char_array.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
88
char arr[] = new char[s.length()];
99
// We limit arbitrarly the loop unfolding to 5
1010
for(int i = 0; i < length && i < 5; i++)
11-
arr[i] = s.charAt(i);
11+
arr[i] = org.cprover.CProverString.charAt(s, i);
1212
return arr;
1313
}
1414

@@ -17,7 +17,7 @@ public static void main(int i)
1717
String s = "abc";
1818
char [] str = toCharArray(s);
1919
char c = str[2];
20-
char a = s.charAt(0);
20+
char a = org.cprover.CProverString.charAt(s, 0);
2121
assert(str.length == 3);
2222
assert(a == 'a');
2323
assert(c == 'c');

‎regression/strings-smoke-tests/java_char_at/test_char_at.class

49 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_char_at/test_char_at.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ public class test_char_at {
22

33
public static void main(/*String[] argv*/) {
44
String s = new String("abc");
5-
assert(s.charAt(2)=='c');
5+
assert(org.cprover.CProverString.charAt(s, 2)=='c');
66
}
77
}

‎regression/strings-smoke-tests/java_code_point/test_code_point.class

91 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_code_point/test_code_point.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,6 @@ public static void main(/*String[] argv*/)
99
assert(s.offsetByCodePoints(1,2) >= 3);
1010
StringBuilder sb = new StringBuilder();
1111
sb.appendCodePoint(0x10907);
12-
assert(s.charAt(1) == sb.charAt(0));
12+
assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));
1313
}
1414
}

‎regression/strings-smoke-tests/java_concat/test_concat.class

49 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_concat/test_concat.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
66
int i = s.length();
77
String t = new String("ppo");
88
String u = s.concat(t);
9-
char c = u.charAt(i);
9+
char c = org.cprover.CProverString.charAt(u, i);
1010
assert(c == 'p');
1111
assert(c == 'o');
1212
}

‎regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class

49 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ public class test_set_char_at
33
public static void main(/*String[] argv*/)
44
{
55
String s = new String("Abc");
6-
char c = s.charAt(1);
6+
char c = org.cprover.CProverString.charAt(s, 1);
77
StringBuilder sb = new StringBuilder(s);
88
sb.setCharAt(1,'w');
99
s = sb.toString();
1010
assert(s.equals("Awc"));
11-
assert(s.charAt(2)=='c');
11+
assert(org.cprover.CProverString.charAt(s, 2)=='c');
1212
}
1313
}

‎regression/strings-smoke-tests/java_substring/test_substring.class

64 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/java_substring/test_substring.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ public class test_substring
33
public static void main(/*String[] argv*/)
44
{
55
String abcdef = "AbcDef";
6-
String cde = abcdef.substring(2,5);
7-
char c = cde.charAt(0);
8-
char d = cde.charAt(1);
9-
char e = cde.charAt(2);
6+
String cde = org.cprover.CProverString.substring(abcdef, 2,5);
7+
char c = org.cprover.CProverString.charAt(cde, 0);
8+
char d = org.cprover.CProverString.charAt(cde, 1);
9+
char e = org.cprover.CProverString.charAt(cde, 2);
1010
assert(c == 'c');
1111
assert(d == 'D');
1212
assert(e == 'e');

‎src/analyses/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
SRC = ai.cpp \
22
call_graph.cpp \
3+
call_graph_helpers.cpp \
34
constant_propagator.cpp \
45
custom_bitvector_analysis.cpp \
56
dependence_graph.cpp \

0 commit comments

Comments
 (0)