Skip to content

Commit 18e6641

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 18e6641

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: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,15 @@ class ClassB {
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 > 0);
2025
return i;
2126
}
2227
}
Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
CORE
22
AbstractTest.class
3-
--cover location --function AbstractTest.getFromAbstract
4-
^EXIT=0$
3+
--function AbstractTest.getFromAbstract
4+
^EXIT=10$
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+
assertion at file AbstractTest.java line 24 .*: FAILURE

0 commit comments

Comments
 (0)