Skip to content

Commit 6901945

Browse files
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
Binary file not shown.
Binary file not shown.
Binary file not shown.
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
}
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

0 commit comments

Comments
 (0)