Skip to content

Commit 9b052c2

Browse files
author
thk123
committed
Modified tests to pass without using grep
Now directly test individual lines with perls regex matching rather than calling out to grep. Some changes were required: - escape (, ) if we want to match them - unescape (, ) if we want to use them as regex bracket groups - escape +, $ if we want to use them as actual characters - unescape + to use as a regex +
1 parent ebe4a7f commit 9b052c2

File tree

213 files changed

+306
-306
lines changed

Some content is hidden

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

213 files changed

+306
-306
lines changed

regression/ansi-c/struct6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33

4-
^EXIT=\(64\|1\)$
4+
^EXIT=(64|1)$
55
^SIGNAL=0$
66
^main.c:2:1: error: incomplete type not permitted here$
77
^CONVERSION ERROR$

regression/ansi-c/struct7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33

4-
^EXIT=\(64\|1\)$
4+
^EXIT=(64|1)$
55
^SIGNAL=0$
66
^main.c:4:1: error: duplicate member .*$
77
^CONVERSION ERROR$

regression/cbmc-concurrency/constant_prop1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
7-
^Generated 1 VCC(s), 0 remaining after simplification$
7+
^Generated 1 VCC\(s\), 0 remaining after simplification$
88
--
99
^warning: ignoring

regression/cbmc-concurrency/pthread_join1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
^SIGNAL=0$
66
^\[main\.assertion\.1\] assertion i==1: FAILURE$
77
^\[main\.assertion\.2\] assertion i==2: SUCCESS$
8-
^\*\* 1 of 2 failed (2 iterations)$
8+
^\*\* 1 of 2 failed \(2 iterations\)$
99
--
1010
^warning: ignoring

regression/cbmc-cover/branch3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33
--cover branch --unwind 6
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 23 of 23 covered (100.0%)$
6+
^\*\* 23 of 23 covered \(100.0%\)$
77
--
88
^warning: ignoring

regression/cbmc-cover/branch4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33
--cover branch
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 1 of 1 covered (100.0%)$
6+
^\*\* 1 of 1 covered \(100.0%\)$
77
--
88
^warning: ignoring

regression/cbmc-cover/condition1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,6 @@ main.c
1313
^\[main.coverage.8] file main.c line 14 function main condition .* true: SATISFIED
1414
^\[main.coverage.9] file main.c line 16 function main condition .* false: FAILED
1515
^\[main.coverage.10] file main.c line 16 function main condition .* true: SATISFIED
16-
^\*\* 9 of 10 covered (90.0%)
16+
^\*\* 9 of 10 covered \(90.0%\)
1717
--
1818
^warning: ignoring

regression/cbmc-cover/cover1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ main.c
66
^\[main.coverage.1] file main.c line 8 function main condition .*: SATISFIED$
77
^\[main.coverage.2] file main.c line 9 function main condition .*: SATISFIED$
88
^\[main.coverage.3] file main.c line 13 function main condition .*: FAILED$
9-
^\*\* 2 of 3 covered (66.7%)$
9+
^\*\* 2 of 3 covered \(66.7%\)$
1010
--
1111
^warning: ignoring

regression/cbmc-cover/decision1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33
--cover decision
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 2 of 2 covered (100.0%)$
6+
^\*\* 2 of 2 covered \(100.0%\)$
77
--
88
^warning: ignoring

regression/cbmc-cover/location1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,6 @@ main.c
88
^\[main.coverage.3\] file main.c line 13 function main block 3: SATISFIED$
99
^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
1010
^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
11-
^\*\* 4 of 5 covered (80.0%)
11+
^\*\* 4 of 5 covered \(80.0%\)
1212
--
1313
^warning: ignoring

regression/cbmc-cover/location11/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@ main.c
1414
^\[main.coverage.9\] file main.c line 23 function main block 10: SATISFIED$
1515
^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
1616
^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
17-
^\*\* 6 of 11 covered (54.5%)
17+
^\*\* 6 of 11 covered \(54.5%\)
1818
--
1919
^warning: ignoring

regression/cbmc-cover/location12/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,6 @@ main.c
1010
^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
1111
^\[foo.coverage.3\] file main.c line 7 function foo block 3: FAILED$
1212
^\[foo.coverage.4\] file main.c line 7 function foo block 4: SATISFIED$
13-
^\*\* 5 of 7 covered (71.4%)
13+
^\*\* 5 of 7 covered \(71.4%\)
1414
--
1515
^warning: ignoring

regression/cbmc-cover/location13/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,6 @@ main.c
1313
^\[foo.coverage.3\] file main.c line 11 function foo block 3: FAILED$
1414
^\[foo.coverage.4\] file main.c line 12 function foo block 4: FAILED$
1515
^\[foo.coverage.5\] file main.c line 12 function foo block 5: SATISFIED$
16-
^\*\* 5 of 10 covered (50.0%)
16+
^\*\* 5 of 10 covered \(50.0%\)
1717
--
1818
^warning: ignoring

regression/cbmc-cover/location14/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,6 @@ main.c
99
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
1010
^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
1111
^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
12-
^\*\* 2 of 6 covered (33.3%)
12+
^\*\* 2 of 6 covered \(33.3%\)
1313
--
1414
^warning: ignoring

regression/cbmc-cover/location15/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,6 @@ main.c
1212
^\[main.coverage.7\] file main.c line 17 function main block 7: SATISFIED$
1313
^\[foo.coverage.1\] file main.c line 6 function foo block 1: FAILED$
1414
^\[foo.coverage.2\] file main.c line 7 function foo block 2: FAILED$
15-
^\*\* 3 of 9 covered (33.3%)
15+
^\*\* 3 of 9 covered \(33.3%\)
1616
--
1717
^warning: ignoring

regression/cbmc-cover/location16/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,6 @@ main.c
1212
^\[func.coverage.5\] file main.c line 13 function func block 5: FAILED$
1313
^\[func.coverage.6\] file main.c line 15 function func block 6: FAILED$
1414
^\[func.coverage.7\] file main.c line 16 function func block 7: SATISFIED$
15-
^\*\* 4 of 9 covered (44.4%)
15+
^\*\* 4 of 9 covered \(44.4%\)
1616
--
1717
^warning: ignoring

regression/cbmc-cover/mcdc1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ main.c
99
^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
1010
^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
1111
^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
12-
^\*\* .* of .* covered (100.0%)$
12+
^\*\* .* of .* covered \(100.0%\)$
1313
^\*\* Used 10 iterations$
1414
--
1515
^warning: ignoring

regression/cbmc-cover/mcdc10/test.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$
9-
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
10-
^\*\* .* of .* covered (100.0%)$
6+
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && !\(C != FALSE\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$
10+
^\*\* .* of .* covered \(100.0%\)$
1111
^\*\* Used 5 iterations$
1212
--
1313
^warning: ignoring

regression/cbmc-cover/mcdc11/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
9-
^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
10-
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
11-
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
12-
^\*\* .* of .* covered (100.0%)$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$
9+
^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$
10+
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
11+
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
12+
^\*\* .* of .* covered \(100.0%\)$
1313
^\*\* Used 6 iterations$
1414
--
1515
^warning: ignoring

regression/cbmc-cover/mcdc12/test.desc

+9-9
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,15 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
9-
^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
10-
^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
11-
^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
12-
^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !(F != FALSE).*: SATISFIED$
13-
^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && F != FALSE.*: SATISFIED$
14-
^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && !(F != FALSE).*: SATISFIED$
15-
^\*\* .* of .* covered (100.0%)$
7+
^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$
9+
^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$
10+
^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
11+
^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
12+
^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !\(F != FALSE\).*: SATISFIED$
13+
^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$
14+
^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$
15+
^\*\* .* of .* covered \(100.0%\)$
1616
^\*\* Used 10 iterations$
1717
--
1818
^warning: ignoring

regression/cbmc-cover/mcdc13/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,10 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$
7-
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !(C != FALSE).* SATISFIED$
8-
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE.* SATISFIED$
9-
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE.* SATISFIED$
10-
^\*\* .* of .* covered (100.0%)$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !\(C != FALSE\).* SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE.* SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE.* SATISFIED$
10+
^\*\* .* of .* covered \(100.0%\)$
1111
^\*\* Used 6 iterations$
1212
--
1313
^warning: ignoring

regression/cbmc-cover/mcdc14/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
77
^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
8-
^\*\* .* of .* covered (100.0%)$
8+
^\*\* .* of .* covered \(100.0%\)$
99
^\*\* Used 2 iterations$
1010
--
1111
^warning: ignoring

regression/cbmc-cover/mcdc2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ main.c
77
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
88
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
99
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
10-
^\*\* .* of .* covered (100.0%)$
10+
^\*\* .* of .* covered \(100.0%\)$
1111
^\*\* Used 6 iterations$
1212
--
1313
^warning: ignoring

regression/cbmc-cover/mcdc3/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
9-
^\*\* .* of .* covered (100.0%)$
6+
^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!\(x > \(unsigned int\)3\) && !\(y < \(unsigned int\)5\).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$
9+
^\*\* .* of .* covered \(100.0%\)$
1010
^\*\* Used 4 iterations$
1111
--
1212
^warning: ignoring

regression/cbmc-cover/mcdc4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ main.c
88
^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
99
^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
1010
^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
11-
^\*\* .* of .* covered (100.0%)$
11+
^\*\* .* of .* covered \(100.0%\)$
1212
^\*\* Used 9 iterations$
1313
--
1414
^warning: ignoring

regression/cbmc-cover/mcdc5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ main.c
88
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
99
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
1010
^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
11-
^\*\* .* of .* covered (100.0%)$
11+
^\*\* .* of .* covered \(100.0%\)$
1212
^\*\* Used 9 iterations$
1313
--
1414
^warning: ignoring

regression/cbmc-cover/mcdc6/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
8-
^\*\* .* of .* covered (100.0%)$
6+
^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$
8+
^\*\* .* of .* covered \(100.0%\)$
99
^\*\* Used 2 iterations$
1010
--
1111
^warning: ignoring

regression/cbmc-cover/mcdc7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ main.c
77
^\[main.coverage.2\] file main.c line 8 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
88
^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
99
^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
10-
^\*\* .* of .* covered (100.0%)$
10+
^\*\* .* of .* covered \(100.0%\)$
1111
^\*\* Used 2 iterations$
1212
--
1313
^warning: ignoring

regression/cbmc-cover/mcdc8/test.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$
7-
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$
8-
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$
9-
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$
10-
^\*\* .* of .* covered (100.0%)$
6+
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
10+
^\*\* .* of .* covered \(100.0%\)$
1111
^\*\* Used 6 iterations$
1212
--
1313
^warning: ignoring

regression/cbmc-cover/mcdc9/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
7-
^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && D != FALSE && A != FALSE && !(B != FALSE).* SATISFIED$
8-
^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE) && A != FALSE && !(B != FALSE).* SATISFIED$
9-
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE && !(D != FALSE).* SATISFIED$
10-
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
11-
^\*\* .* of .* covered (100.0%)$
6+
^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
7+
^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE && A != FALSE && !\(B != FALSE\).* SATISFIED$
8+
^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\) && A != FALSE && !\(B != FALSE\).* SATISFIED$
9+
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$
10+
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
11+
^\*\* .* of .* covered \(100.0%\)$
1212
^\*\* Used 8 iterations$
1313
--
1414
^warning: ignoring

regression/cbmc-java/LocalVarTable2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ LocalVarTable2.class
44
^EXIT=0$
55
^SIGNAL=0$
66
--
7-
return_value.*(void \*)i
7+
return_value.*\(void \*\)i

regression/cbmc-java/NullPointer1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer1.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer1.java line 16 function java::NullPointer1.main:(\[Ljava/lang/String;)V$
6+
^ file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

regression/cbmc-java/NullPointer2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer2.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V
6+
^ file NullPointer2.java line 9 function java::NullPointer2.main:\(\[Ljava/lang/String;\)V
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

regression/cbmc-java/NullPointer3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer3.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer3.java line 5 function java::NullPointer3.main:(\[Ljava/lang/String;)V bytecode_index 1$
6+
^ file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

regression/cbmc-java/NullPointer4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer4.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer4.java line 6 function java::NullPointer4.main:(\[Ljava/lang/String;)V$
6+
^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

regression/cbmc-java/VarLengthArrayTrace1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,4 @@ dynamic_3_array\[1l\]=10
77
--
88
^warning: ignoring
99
assignment removed
10-
irep("(\\"nil\\")")
10+
irep\("\(\\"nil\\"\)"\)

regression/cbmc-java/enum1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ enum1.class
33
--java-unwind-enum-static --unwind 3
44
^EXIT=10$
55
^SIGNAL=0$
6-
^Unwinding loop java::enum1.<clinit>:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.<clinit>:()V bytecode_index 78 thread 0$
6+
^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode_index 78 thread 0$
77
--
88
^warning: ignoring

0 commit comments

Comments
 (0)