Skip to content

Commit 8c862d1

Browse files
committed
Fixed cbmc-cover regressions
1 parent 3f4625c commit 8c862d1

File tree

18 files changed

+18
-18
lines changed

18 files changed

+18
-18
lines changed

regression/cbmc-cover/block-coverage-report2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location
3+
--no-standard-checks --cover location
44
block 1 \(lines main.c:main:13,14\): SATISFIED
55
block 2 \(lines main.c:main:15\): SATISFIED
66
block 3 \(lines main.c:main:17,18\): SATISFIED

regression/cbmc-cover/block-coverage-report3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location --unwind 1
3+
--no-standard-checks --cover location --unwind 1
44
block 1 \(lines main.c:main:3\): SATISFIED
55
block 2 \(lines main.c:main:4\): SATISFIED
66
block 3 \(lines main.c:main:4,6\): SATISFIED

regression/cbmc-cover/block-coverage-report4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location --unwind 4
3+
--no-standard-checks --cover location --unwind 4
44
block 1 \(lines main.c:main:3\): SATISFIED
55
block 2 \(lines main.c:main:4\): SATISFIED
66
block 3 \(lines main.c:main:4,6\): SATISFIED

regression/cbmc-cover/built-ins1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location --unwind 1
3+
--no-standard-checks --cover location --unwind 1
44
^EXIT=0$
55
^SIGNAL=0$
66
^\*\* 5 of 7 covered

regression/cbmc-cover/built-ins4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover branch --unwind 5
3+
--no-standard-checks --cover branch --unwind 5
44
^EXIT=0$
55
^SIGNAL=0$
66
^\*\* 5 of 5 covered

regression/cbmc-cover/built-ins5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover condition --unwind 5
3+
--no-standard-checks --cover condition --unwind 5
44
^EXIT=0$
55
^SIGNAL=0$
66
^\*\* 4 of 4 covered

regression/cbmc-cover/built-ins6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover decision --unwind 5
3+
--no-standard-checks --cover decision --unwind 5
44
^EXIT=0$
55
^SIGNAL=0$
66
^\*\* 4 of 4 covered

regression/cbmc-cover/built-ins7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover mcdc --unwind 5
3+
--no-standard-checks --cover mcdc --unwind 5
44
^EXIT=0$
55
^SIGNAL=0$
66
^\*\* 4 of 4 covered

regression/cbmc-cover/location-assume/middle.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
middle.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file middle.c line 5 function main block 1 \(lines middle\.c:main:5-8\): SATISFIED$

regression/cbmc-cover/location-multiline-statement/multi-file.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
multi-file.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.2\] file multi-file.c line 10 function main block 2 \(lines [\w\- /\.\\:]*dereference.h:main:2; multi-file.c:main:10,13,14,16\): SATISFIED

regression/cbmc-cover/location-multiline-statement/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
example.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.2\] file example.c line 10 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$

regression/cbmc-cover/location11/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 9 function main block 1.*: SATISFIED$

regression/cbmc-cover/location12/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 9 function main block 1.*: SATISFIED$

regression/cbmc-cover/location13/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 14 function main block 1.*: SATISFIED$

regression/cbmc-cover/location14/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 8 function main block 1.*: SATISFIED$

regression/cbmc-cover/location16/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover location
3+
--no-standard-checks --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 19 function main block 1.*: SATISFIED$

regression/cbmc-cover/mcdc7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--cover mcdc
3+
--no-standard-checks --cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 8 function main decision/condition 'x \* 123 > 100.* false: SATISFIED$

regression/cbmc-cover/pointer-function-parameters-struct-simple-recursion-3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--function func --min-null-tree-depth 2 --max-nondet-tree-depth 10 --cover branch
3+
--no-standard-checks --function func --min-null-tree-depth 2 --max-nondet-tree-depth 10 --cover branch
44
^EXIT=0$
55
^SIGNAL=0$
66
\[func.coverage.2\] file main.c line .* function func block 1 branch false: SATISFIED

0 commit comments

Comments
 (0)