Skip to content

Commit 6901945

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 6901945

File tree

125 files changed

+342
-315
lines changed

Some content is hidden

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

125 files changed

+342
-315
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$ClassA.class

0 Bytes
Binary file not shown.

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

10 Bytes
Binary file not shown.

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

0 Bytes
Binary file not shown.

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

298 Bytes
Binary file not shown.

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

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,19 @@ public class AbstractTest {
99
class Dummy { private boolean b; }
1010
class ClassA { private int id; }
1111
class ClassB {
12-
private int id;
12+
private int id = 42;
1313
int getId() { return id; }
1414
}
1515

16-
public int getFromAbstract(AbstractInt<ClassA, ClassB> arg) {
16+
public int getFromAbstract(AbstractImpl<ClassA, ClassB> arg) {
17+
if (arg == null)
18+
return -1;
1719
AbstractImpl<Dummy, Dummy> dummy = new AbstractImpl<>();
1820
ClassB b = arg.get();
21+
if (b == null)
22+
return -1;
1923
int i = b.getId();
24+
assert(i == 42);
2025
return i;
2126
}
2227
}

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

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
CORE
22
AbstractTest.class
3-
--cover location --function AbstractTest.getFromAbstract
3+
--function AbstractTest.getFromAbstract
44
^EXIT=0$
55
^SIGNAL=0$
6-
file AbstractTest.java line 18 .* SATISFIED
7-
file AbstractTest.java line 19 .* SATISFIED
8-
file AbstractTest.java line 20 .* SATISFIED
9-
file AbstractTest.java line 21 .* SATISFIED
6+
^VERIFICATION SUCCESSFUL

‎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

Lines changed: 6 additions & 2 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 6 additions & 2 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 6 additions & 2 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 2 additions & 0 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 7 additions & 2 deletions
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

Lines changed: 6 additions & 3 deletions
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

Lines changed: 10 additions & 2 deletions
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

Lines changed: 4 additions & 16 deletions
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

Lines changed: 4 additions & 17 deletions
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

Lines changed: 1 addition & 2 deletions
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

Lines changed: 4 additions & 0 deletions
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.

0 commit comments

Comments
 (0)