Skip to content

Commit 105c7e3

Browse files
Adapt coverage test for new instrumentation
JBMC use to group together several lines within the same block. This is no longer the case for the Java specific block instrumentation. Each line is part of a different goal.
1 parent c1045aa commit 105c7e3

File tree

1 file changed

+10
-1
lines changed

1 file changed

+10
-1
lines changed

regression/cbmc-java/covered1/test.desc

+10-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,16 @@ covered1.class
44
^EXIT=0$
55
^SIGNAL=0$
66
.*\"coveredLines\": \"22\",$
7-
.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$
7+
.*\"coveredLines\": \"4\",$
8+
.*\"coveredLines\": \"6\",$
9+
.*\"coveredLines\": \"7\",$
10+
.*\"coveredLines\": \"23\",$
11+
.*\"coveredLines\": \"24\",$
12+
.*\"coveredLines\": \"25\",$
13+
.*\"coveredLines\": \"31\",$
14+
.*\"coveredLines\": \"32\",$
15+
.*\"coveredLines\": \"33\",$
16+
.*\"coveredLines\": \"36\",$
817
.*\"coveredLines\": \"26\",$
918
.*\"coveredLines\": \"28\",$
1019
.*\"coveredLines\": \"28\",$

0 commit comments

Comments
 (0)