Skip to content

Commit 0cccfe3

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #505 from thk123/bug/support-multi-line-mac
Test runner Perl script not using grep
2 parents 2654d7b + 9b052c2 commit 0cccfe3

File tree

229 files changed

+509
-330
lines changed

Some content is hidden

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

229 files changed

+509
-330
lines changed

‎regression/Makefile

+9-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,13 @@
11

2-
DIRS = ansi-c cbmc cpp goto-instrument goto-analyzer cbmc-java
2+
DIRS = ansi-c \
3+
cbmc \
4+
cpp \
5+
cbmc-java \
6+
goto-analyzer \
7+
goto-instrument \
8+
test-script \
9+
# Empty last line
10+
311

412
test:
513
$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)

‎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\\"\)"\)

0 commit comments

Comments
 (0)