Skip to content

Commit e152c92

Browse files
peterschrammelpeterschrammel
committed
JBMC tests should not use --cover
Use assertions instead. Tests that make only sense with --cover are moved to jbmc-cover.
1 parent 049dd2f commit e152c92

File tree

129 files changed

+345
-318
lines changed

Some content is hidden

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

129 files changed

+345
-318
lines changed

‎jbmc/regression/jbmc/covered1/covered1.class renamed to ‎jbmc/regression/jbmc-cover/covered1/covered1.class

File renamed without changes.

‎jbmc/regression/jbmc/covered1/covered1.java renamed to ‎jbmc/regression/jbmc-cover/covered1/covered1.java

File renamed without changes.

‎jbmc/regression/jbmc/covered1/test.desc renamed to ‎jbmc/regression/jbmc-cover/covered1/test.desc

File renamed without changes.

‎jbmc/regression/jbmc-cover/generics/AbstractTest.class

-645 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-cover/generics/test.desc

-9
This file was deleted.

‎jbmc/regression/jbmc/json_trace2/Test.class renamed to ‎jbmc/regression/jbmc-cover/json_trace2/Test.class

File renamed without changes.

‎jbmc/regression/jbmc/json_trace2/Test.java renamed to ‎jbmc/regression/jbmc-cover/json_trace2/Test.java

File renamed without changes.

‎jbmc/regression/jbmc/json_trace2/test.desc renamed to ‎jbmc/regression/jbmc-cover/json_trace2/test.desc

File renamed without changes.

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

93 Bytes
Binary file not shown.

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

+6-2
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ public String det()
1818
builder.setCharAt(11, ':');
1919
builder.setCharAt(16, ':');
2020
builder.setCharAt(18, ':');
21-
return builder.toString();
21+
String result = builder.toString();
22+
assert result.length() < 5;
23+
return result;
2224
}
2325

2426
public String nonDet(String s, char c, int i)
@@ -42,7 +44,9 @@ public String nonDet(String s, char c, int i)
4244
builder.setCharAt(11, ':');
4345
builder.setCharAt(16, ':');
4446
builder.setCharAt(18, ':');
45-
return builder.toString();
47+
String result = builder.toString();
48+
assert result.length() < 5;
49+
return result;
4650
}
4751

4852
public String withDependency(boolean b)

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Test.class
33
--function Test.withDependency --max-nondet-string-length 1000
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file Test.java line 55 .*: SUCCESS
7-
assertion at file Test.java line 57 .*: FAILURE
6+
assertion at file Test.java line 59 .*: SUCCESS
7+
assertion at file Test.java line 61 .*: FAILURE
88
--
99
--
1010
Check that when a dependency is present, the correct constraints are added

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.det --verbosity 10 --cover location
4-
^EXIT=0$
3+
--function Test.det --verbosity 10
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 21 .*: SATISFIED
6+
assertion at file Test.java line 22 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

‎jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4-
^EXIT=0$
3+
--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 45 .*: SATISFIED
6+
assertion at file Test.java line 48 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

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

93 Bytes
Binary file not shown.

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

+6-2
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,9 @@ public String det()
77
builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toLowerCase());
88
builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toLowerCase());
99
builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toLowerCase());
10-
return builder.toString();
10+
String result = builder.toString();
11+
assert result.length() < 5;
12+
return result;
1113
}
1214

1315
public String nonDet(String s)
@@ -25,7 +27,9 @@ public String nonDet(String s)
2527
builder.append(":");
2628
builder.append(s.toLowerCase());
2729
builder.append(s.toLowerCase());
28-
return builder.toString();
30+
String result = builder.toString();
31+
assert result.length() < 5;
32+
return result;
2933
}
3034

3135
public String withDependency(String s, boolean b)

‎jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Test.class
33
--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file Test.java line 44 .*: SUCCESS
7-
assertion at file Test.java line 46 .*: FAILURE
6+
assertion at file Test.java line 48 .*: SUCCESS
7+
assertion at file Test.java line 50 .*: FAILURE
88
--
99
--
1010
Check that when there are dependencies, axioms are adde correctly.

‎jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.det --verbosity 10 --cover location
4-
^EXIT=0$
3+
--function Test.det --verbosity 10
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 9 .*: SATISFIED
6+
assertion at file Test.java line 11 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

‎jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4-
^EXIT=0$
3+
--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 27 .*: SATISFIED
6+
assertion at file Test.java line 31 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

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

93 Bytes
Binary file not shown.

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

+6-2
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,9 @@ public String det()
77
builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase());
88
builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase());
99
builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase());
10-
return builder.toString();
10+
String result = builder.toString();
11+
assert result.length() < 5;
12+
return result;
1113
}
1214

1315
public String nonDet(String s)
@@ -25,7 +27,9 @@ public String nonDet(String s)
2527
builder.append(":");
2628
builder.append(s.toUpperCase());
2729
builder.append(s.toUpperCase());
28-
return builder.toString();
30+
String result = builder.toString();
31+
assert result.length() < 5;
32+
return result;
2933
}
3034

3135
public String withDependency(String s, boolean b)

‎jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Test.class
33
--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file Test.java line 44 .*: SUCCESS
7-
assertion at file Test.java line 46 .*: FAILURE
6+
assertion at file Test.java line 48 .*: SUCCESS
7+
assertion at file Test.java line 50 .*: FAILURE
88
--
99
--
1010
Check that when there are dependencies, axioms are added correctly.

‎jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.det --verbosity 10 --cover location
4-
^EXIT=0$
3+
--function Test.det --verbosity 10
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 9 .*: SATISFIED
6+
assertion at file Test.java line 11 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

‎jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
4-
^EXIT=0$
3+
--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 27 .*: SATISFIED
6+
assertion at file Test.java line 31 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

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

105 Bytes
Binary file not shown.

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

+2
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ public static String checkDet()
2323
tmp = String.valueOf(-1000003);
2424
tmp = String.valueOf(1000004);
2525
tmp = String.valueOf(1000005);
26+
assert tmp.length() < 5;
2627
return tmp;
2728
}
2829

@@ -51,6 +52,7 @@ public static String checkNonDet(int i)
5152
tmp += String.valueOf(-i + 1);
5253
tmp += " ";
5354
tmp += String.valueOf(-i - 2);
55+
assert tmp.length() < 5;
5456
return tmp;
5557
}
5658

‎jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Test.class
33
--function Test.checkWithDependency --depth 10000
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file Test.java line 61 .*: SUCCESS
7-
assertion at file Test.java line 64 .*: FAILURE
6+
assertion at file Test.java line 63 .*: SUCCESS
7+
assertion at file Test.java line 66 .*: FAILURE
88
--
99
--
1010
Check that when a dependency is present, the correct constraints are added

‎jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.checkDet --verbosity 10 --cover location
4-
^EXIT=0$
3+
--function Test.checkDet --verbosity 10
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 25 .*: SATISFIED
6+
assertion at file Test.java line 26 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

‎jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.checkNonDet --verbosity 10 --cover location
4-
^EXIT=0$
3+
--function Test.checkNonDet --verbosity 10
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* file Test.java line 53 .*: SATISFIED
6+
assertion at file Test.java line 55 .*: FAILURE
77
--
88
adding lemma .*nondet_infinite_array
99
--

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

275 Bytes
Binary file not shown.

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

+7-2
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,15 @@ public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6,
1010
sb.append(c6);
1111
sb.append(c7);
1212
sb.append(c8);
13-
if (sb.toString().equals("\b\t\n\f\r\"\'\\"))
13+
if (sb.toString().equals("\b\t\n\f\r\"\'\\")) {
14+
assert false;
1415
return true;
15-
if (!sb.toString().equals("\b\t\n\f\r\"\'\\"))
16+
}
17+
if (!sb.toString().equals("\b\t\n\f\r\"\'\\")) {
18+
assert false;
1619
return false;
20+
}
21+
assert false;
1722
return true;
1823
}
1924
}

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

+6-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
CORE
22
Test.class
3-
--function Test.test --cover location --trace --json-ui
4-
^EXIT=0$
3+
--function Test.test --trace --json-ui
4+
^EXIT=10$
55
^SIGNAL=0$
6-
20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)
6+
"reason": "assertion at file Test.java line 14
7+
"reason": "assertion at file Test.java line 18
8+
--
9+
"reason": "assertion at file Test.java line 21

‎jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class

302 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java

+10-2
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,23 @@ public static Boolean testMyGenSet(Integer key) {
44
if (key == null) return null;
55
MyGenSet<Integer> ms = new MyGenSet<>();
66
ms.array[0] = 101;
7-
if (ms.contains(key)) return true;
7+
if (ms.contains(key)) {
8+
assert false;
9+
return true;
10+
}
11+
assert false;
812
return false;
913
}
1014

1115
public static Boolean testMySet(Integer key) {
1216
if (key == null) return null;
1317
MySet ms = new MySet();
1418
ms.array[0] = 101;
15-
if (ms.contains(key)) return true;
19+
if (ms.contains(key)) {
20+
assert false;
21+
return true;
22+
}
23+
assert false;
1624
return false;
1725
}
1826

‎jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-strings/max-length-generic-array/MySet.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-strings/max-length-generic-array/test.desc

+4-16
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,7 @@
11
CORE
22
IntegerTests.class
3-
--max-nondet-string-length 100 --function IntegerTests.testMySet --cover location
4-
^EXIT=0$
3+
--max-nondet-string-length 100 --function IntegerTests.testMySet
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED
7-
coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED
8-
coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED
9-
coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED
10-
coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED
11-
coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED
12-
coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED
13-
coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED
14-
coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED
15-
coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED
16-
coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED
17-
coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED
18-
coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED
19-
coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED
6+
assertion at file IntegerTests.java line 20 .*: FAILURE
7+
assertion at file IntegerTests.java line 23 .*: FAILURE

‎jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc

+4-17
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,7 @@
11
CORE
22
IntegerTests.class
3-
--max-nondet-string-length 100 --function IntegerTests.testMyGenSet --cover location
4-
^EXIT=0$
3+
--max-nondet-string-length 100 --function IntegerTests.testMyGenSet
4+
^EXIT=10$
55
^SIGNAL=0$
6-
coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED
7-
coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED
8-
coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED
9-
coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED
10-
coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED
11-
coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED
12-
coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED
13-
coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED
14-
coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED
15-
coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED
16-
coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED
17-
coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED
18-
coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED
19-
coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED
20-
coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED
6+
assertion at file IntegerTests.java line 8 .*: FAILURE
7+
assertion at file IntegerTests.java line 11 .*: FAILURE

‎jbmc/regression/jbmc/array2/test.class

276 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/array2/test.desc

+1-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
test.class
3-
--function test.f --cover location
4-
\d+ of \d+ covered
3+
--function test.f
54
^EXIT=0$
65
^SIGNAL=0$
76
--

‎jbmc/regression/jbmc/array2/test.java

+4
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,10 @@ public void f(int unknown) {
1111
if(unknown > 0)
1212
arr[0]=1;
1313

14+
if(unknown > 0)
15+
assert arr[0] == 1;
16+
else
17+
assert arr.length == 0;
1418
}
1519

1620
}

‎jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class

101 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
11
public class FloatMultidim1 {
22
public float[][] f(int y) {
3+
float[][] a1 = null;
34
if (y > 0 && y < 5) {
4-
float[][] a1 = new float[y][2];
5+
a1 = new float[y][2];
56
int j;
67
if (y > 1) {
78
j = 1;
89
} else {
910
j = 0;
1011
}
1112
a1[j][1] = 1.0f;
12-
return a1;
13-
} else {
14-
return null;
1513
}
14+
assert a1 == null;
15+
return a1;
1616
}
1717
}

‎jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class

99 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)