Skip to content

Commit d7cb110

Browse files
mmueslymmuesly
committed
adapt regression tests to changes
1 parent e3c1a68 commit d7cb110

File tree

13 files changed

+39
-39
lines changed

13 files changed

+39
-39
lines changed

‎regression/cbmc-cover/mcdc10/test.desc

Lines changed: 4 additions & 4 deletions
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 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$
6+
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != 0 && !\(B != 0\) && !\(C != 0\).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!\(A != 0\) && B != 0 && !\(C != 0\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!\(A != 0\) && !\(B != 0\) && C != 0.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != 0\) && !\(B != 0\) && !\(C != 0\).*: SATISFIED$
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring

‎regression/cbmc-cover/mcdc11/test.desc

Lines changed: 6 additions & 6 deletions
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.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$
6+
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != 0 && B != 0.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != 0 && !\(B != 0\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!\(A != 0\) && B != 0.*: SATISFIED$
9+
^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != 0 && !\(D != 0\).*: SATISFIED$
10+
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != 0\) && D != 0.*: SATISFIED$
11+
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != 0\) && !\(D != 0\).*: SATISFIED$
1212
^\*\* .* of .* covered \(100.0%\)$
1313
--
1414
^warning: ignoring

‎regression/cbmc-cover/mcdc12/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[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$
6+
^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != 0 && B != 0.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != 0 && !\(B != 0\).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!\(A != 0\) && B != 0.*: SATISFIED$
9+
^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != 0 && !\(D != 0\).*: SATISFIED$
10+
^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!\(C != 0\) && D != 0.*: SATISFIED$
11+
^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!\(C != 0\) && !\(D != 0\).*: SATISFIED$
12+
^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != 0 && !\(F != 0\).*: SATISFIED$
13+
^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != 0\) && F != 0.*: SATISFIED$
14+
^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != 0\) && !\(F != 0\).*: SATISFIED$
1515
^\*\* .* of .* covered \(100.0%\)$
1616
--
1717
^warning: ignoring

‎regression/cbmc-cover/mcdc13/test.desc

Lines changed: 4 additions & 4 deletions
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 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$
6+
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != 0 && B != 0 && C != 0.* SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != 0 && B != 0 && !\(C != 0\).* SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != 0 && !\(B != 0\) && C != 0.* SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != 0\) && B != 0 && C != 0.* SATISFIED$
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring

‎regression/cbmc-cover/mcdc8/test.desc

Lines changed: 4 additions & 4 deletions
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 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$
6+
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != 0 && a != 0 && !\(b != 0\).* SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != 0 && !\(a != 0\) && b != 0.* SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != 0 && !\(a != 0\) && !\(b != 0\).* SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != 0\) && a != 0 && !\(b != 0\).* SATISFIED$
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring

‎regression/cbmc-cover/mcdc9/test.desc

Lines changed: 5 additions & 5 deletions
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.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$
6+
^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != 0 && !\(B != 0\) && C != 0 && !\(D != 0\).* SATISFIED$
7+
^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!\(C != 0\) && D != 0 && A != 0 && !\(B != 0\).* SATISFIED$
8+
^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!\(C != 0\) && !\(D != 0\) && A != 0 && !\(B != 0\).* SATISFIED$
9+
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != 0\) && B != 0 && C != 0 && !\(D != 0\).* SATISFIED$
10+
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != 0\) && !\(B != 0\) && C != 0 && !\(D != 0\).* SATISFIED$
1111
^\*\* .* of .* covered \(100.0%\)$
1212
--
1313
^warning: ignoring

‎regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^\s*IF fp == f2 THEN GOTO [0-9]$
66
^\s*IF fp == f3 THEN GOTO [0-9]$
77
^\s*IF fp == f4 THEN GOTO [0-9]$
8-
^\s*ASSERT FALSE // invalid function pointer$
8+
^\s*ASSERT 0 // invalid function pointer$
99
^EXIT=0$
1010
^SIGNAL=0$
1111
--

‎regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*ASSERT FALSE // invalid function pointer$
5+
^\s*ASSERT 0 // invalid function pointer$
66
^EXIT=0$
77
^SIGNAL=0$
88
function func: replacing function pointer by 0 possible targets

‎regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*ASSERT FALSE // invalid function pointer$
5+
^\s*ASSERT 0 // invalid function pointer$
66
^EXIT=0$
77
^SIGNAL=0$
88
replacing function pointer by 0 possible targets

‎regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*ASSERT FALSE // invalid function pointer$
5+
^\s*ASSERT 0 // invalid function pointer$
66
replacing function pointer by 9 possible targets
77
^EXIT=0$
88
^SIGNAL=0$

‎regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*ASSERT FALSE // invalid function pointer$
5+
^\s*ASSERT 0 // invalid function pointer$
66
replacing function pointer by 9 possible targets
77
^EXIT=0$
88
^SIGNAL=0$

‎regression/goto-analyzer/no-match-const-fp-null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*ASSERT FALSE // invalid function pointer$
5+
^\s*ASSERT 0 // invalid function pointer$
66
function func: replacing function pointer by 0 possible targets
77
^EXIT=0$
88
^SIGNAL=0$

‎regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*ASSERT FALSE // invalid function pointer$
5+
^\s*ASSERT 0 // invalid function pointer$
66
^EXIT=0$
77
^SIGNAL=0$
88
replacing function pointer by 0 possible targets

0 commit comments

Comments
 (0)