From a14f4a36b373f7359d57a1d23e2480323e9ff1bf Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 21 Oct 2016 12:07:15 +0100 Subject: [PATCH 01/15] add test case mcdc8 to test MC/DC coverage instrumentation Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc8/main.c | 19 +++++++++++++++++++ regression/cbmc-cover/mcdc8/test.desc | 13 +++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 regression/cbmc-cover/mcdc8/main.c create mode 100644 regression/cbmc-cover/mcdc8/test.desc diff --git a/regression/cbmc-cover/mcdc8/main.c b/regression/cbmc-cover/mcdc8/main.c new file mode 100644 index 00000000000..3eb9a0010e9 --- /dev/null +++ b/regression/cbmc-cover/mcdc8/main.c @@ -0,0 +1,19 @@ +int main() +{ + _Bool a, b, c; + + __CPROVER_input("a", a); + __CPROVER_input("b", b); + __CPROVER_input("c", c); + + if ( (a || b) && c ) + { + /* instructions */ + } + else + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc new file mode 100644 index 00000000000..c1dad51b9b4 --- /dev/null +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^a=TRUE, b=FALSE, c=TRUE$ +^a=TRUE, b=FALSE, c=FALSE$ +^a=FALSE, b=FALSE, c=FALSE$ +^a=FALSE, b=TRUE, c=FALSE$ +^a=FALSE, b=TRUE, c=TRUE$ +^a=FALSE, b=FALSE, c=TRUE$ +-- +^warning: ignoring From 977ea0225cd86cdff51fdfbcd09beee5468e7ef1 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 21 Oct 2016 12:26:58 +0100 Subject: [PATCH 02/15] add test case mcdc9 to test MC/DC coverage instrumentation Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc9/main.c | 26 ++++++++++++++++++++++++++ regression/cbmc-cover/mcdc9/test.desc | 17 +++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 regression/cbmc-cover/mcdc9/main.c create mode 100644 regression/cbmc-cover/mcdc9/test.desc diff --git a/regression/cbmc-cover/mcdc9/main.c b/regression/cbmc-cover/mcdc9/main.c new file mode 100644 index 00000000000..f239e63f287 --- /dev/null +++ b/regression/cbmc-cover/mcdc9/main.c @@ -0,0 +1,26 @@ +int main() +{ + _Bool u, x, y, z; + _Bool A, B, C, D; + + A = (u==0); + B = (x>5); + C = (y<6); + D = (z==0); + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + + if ( (A || B) && (C || D) ) + { + /* instructions */ + } + else + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc new file mode 100644 index 00000000000..89f01dcf35c --- /dev/null +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -0,0 +1,17 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^A=FALSE, B=FALSE, C=FALSE, D=FALSE$ +^A=FALSE, B=TRUE, C=FALSE, D=TRUE$ +^A=TRUE, B=FALSE, C=TRUE, D=TRUE$ +^A=TRUE, B=FALSE, C=TRUE, D=FALSE$ +^A=TRUE, B=FALSE, C=FALSE, D=FALSE$ +^A=TRUE, B=FALSE, C=FALSE, D=TRUE$ +^A=FALSE, B=FALSE, C=FALSE, D=TRUE$ +^A=FALSE, B=TRUE, C=FALSE, D=FALSE$ +^A=FALSE, B=TRUE, C=TRUE, D=FALSE$ +^A=FALSE, B=FALSE, C=TRUE, D=FALSE$ +-- +^warning: ignoring From 3bffc8e13e5f73378720c380875b8e210f0de88d Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 21 Oct 2016 15:58:48 +0100 Subject: [PATCH 03/15] update test case mcdc9 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc9/test.desc | 2 -- 1 file changed, 2 deletions(-) diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc index 89f01dcf35c..ef0b713cafc 100644 --- a/regression/cbmc-cover/mcdc9/test.desc +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -3,8 +3,6 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^A=FALSE, B=FALSE, C=FALSE, D=FALSE$ -^A=FALSE, B=TRUE, C=FALSE, D=TRUE$ ^A=TRUE, B=FALSE, C=TRUE, D=TRUE$ ^A=TRUE, B=FALSE, C=TRUE, D=FALSE$ ^A=TRUE, B=FALSE, C=FALSE, D=FALSE$ From 87adf3bf324d73efbc296031f542970577d11fa7 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 21 Oct 2016 16:27:47 +0100 Subject: [PATCH 04/15] update test case mcdc10 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc10/main.c | 19 +++++++++++++++++++ regression/cbmc-cover/mcdc10/test.desc | 11 +++++++++++ 2 files changed, 30 insertions(+) create mode 100644 regression/cbmc-cover/mcdc10/main.c create mode 100644 regression/cbmc-cover/mcdc10/test.desc diff --git a/regression/cbmc-cover/mcdc10/main.c b/regression/cbmc-cover/mcdc10/main.c new file mode 100644 index 00000000000..703132cb4f2 --- /dev/null +++ b/regression/cbmc-cover/mcdc10/main.c @@ -0,0 +1,19 @@ +int main() +{ + _Bool A, B, C; + + __CPROVER_input("cold", A); + __CPROVER_input("raining", B); + __CPROVER_input("windy", C); + + if ( A || B || C ) + { + /* instructions */ + } + else + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc new file mode 100644 index 00000000000..7df6b51ffac --- /dev/null +++ b/regression/cbmc-cover/mcdc10/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$ +-- +^warning: ignoring From 01830b53b7dfcbdef72158347f9b1809d44f3ccd Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 21 Oct 2016 16:50:41 +0100 Subject: [PATCH 05/15] add test case mcdc11 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc11/main.c | 27 ++++++++++++++++++++++++++ regression/cbmc-cover/mcdc11/test.desc | 13 +++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 regression/cbmc-cover/mcdc11/main.c create mode 100644 regression/cbmc-cover/mcdc11/test.desc diff --git a/regression/cbmc-cover/mcdc11/main.c b/regression/cbmc-cover/mcdc11/main.c new file mode 100644 index 00000000000..fc4970ab459 --- /dev/null +++ b/regression/cbmc-cover/mcdc11/main.c @@ -0,0 +1,27 @@ +int main() +{ + _Bool A, B, C, D; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + + if (A && B) + { + if (C || D) + { + /* instructions */ + } + else + { + /* instructions */ + } + } + else + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc new file mode 100644 index 00000000000..5a8585e1554 --- /dev/null +++ b/regression/cbmc-cover/mcdc11/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$ +^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$ +^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$ +^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$ +-- +^warning: ignoring From 454a38ae63a28780b106540f77c367726691aea4 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 21 Oct 2016 16:57:17 +0100 Subject: [PATCH 06/15] add test case mcdc12 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc12/main.c | 36 ++++++++++++++++++++++++++ regression/cbmc-cover/mcdc12/test.desc | 16 ++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 regression/cbmc-cover/mcdc12/main.c create mode 100644 regression/cbmc-cover/mcdc12/test.desc diff --git a/regression/cbmc-cover/mcdc12/main.c b/regression/cbmc-cover/mcdc12/main.c new file mode 100644 index 00000000000..f0f79018416 --- /dev/null +++ b/regression/cbmc-cover/mcdc12/main.c @@ -0,0 +1,36 @@ +int main() +{ + _Bool A, B, C, D, E, F; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + __CPROVER_input("E", D); + __CPROVER_input("F", D); + + if (A && B) + { + if (C || D) + { + /* instructions */ + } + else + { + /* instructions */ + } + } + else + { + if (E || F) + { + /* instructions */ + } + else + { + /* instructions */ + } + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc new file mode 100644 index 00000000000..37779f1f821 --- /dev/null +++ b/regression/cbmc-cover/mcdc12/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$ +^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$ +^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$ +^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$ +^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !(F != FALSE).*: SATISFIED$ +^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && F != FALSE.*: SATISFIED$ +^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && !(F != FALSE).*: SATISFIED$ +-- +^warning: ignoring From 06c0d379acc4ccc85e61fbb34d1f3a63fef6961f Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 13:54:21 +0100 Subject: [PATCH 07/15] add test case mcdc13 to test AND gate Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc13/main.c | 14 ++++++++++++++ regression/cbmc-cover/mcdc13/test.desc | 11 +++++++++++ 2 files changed, 25 insertions(+) create mode 100644 regression/cbmc-cover/mcdc13/main.c create mode 100644 regression/cbmc-cover/mcdc13/test.desc diff --git a/regression/cbmc-cover/mcdc13/main.c b/regression/cbmc-cover/mcdc13/main.c new file mode 100644 index 00000000000..b26bef260cc --- /dev/null +++ b/regression/cbmc-cover/mcdc13/main.c @@ -0,0 +1,14 @@ +int main() +{ + _Bool A, B; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + + if (A && B) + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc new file mode 100644 index 00000000000..3d99dd739ff --- /dev/null +++ b/regression/cbmc-cover/mcdc13/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^A=FALSE, B=TRUE$ +^A=FALSE, B=FALSE$ +^A=TRUE, B=FALSE$ +^A=TRUE, B=TRUE$ +-- +^warning: ignoring From 5a19b121fbeba0544342f2894a1faa9b8d3dffb6 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:05:40 +0100 Subject: [PATCH 08/15] add test case mcdc14 to test OR gate Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc14/main.c | 17 +++++++++++++++++ regression/cbmc-cover/mcdc14/test.desc | 11 +++++++++++ 2 files changed, 28 insertions(+) create mode 100644 regression/cbmc-cover/mcdc14/main.c create mode 100644 regression/cbmc-cover/mcdc14/test.desc diff --git a/regression/cbmc-cover/mcdc14/main.c b/regression/cbmc-cover/mcdc14/main.c new file mode 100644 index 00000000000..496ddb0c70d --- /dev/null +++ b/regression/cbmc-cover/mcdc14/main.c @@ -0,0 +1,17 @@ +int main() +{ + _Bool A, B, C; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_output("C", C); + + C = (A || B); + + if (C) + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc new file mode 100644 index 00000000000..fc7c64c0396 --- /dev/null +++ b/regression/cbmc-cover/mcdc14/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^A=TRUE, B=FALSE$ +^A=TRUE, B=TRUE$ +^A=FALSE, B=TRUE$ +^A=FALSE, B=FALSE$ +-- +^warning: ignoring From f239e0a94d36a50c370dbba54e1f1ca0a20b8f77 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:21:23 +0100 Subject: [PATCH 09/15] fix test desc of mcdc8 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc8/test.desc | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index c1dad51b9b4..bf8dabbfa0f 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -3,11 +3,11 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^a=TRUE, b=FALSE, c=TRUE$ -^a=TRUE, b=FALSE, c=FALSE$ -^a=FALSE, b=FALSE, c=FALSE$ -^a=FALSE, b=TRUE, c=FALSE$ -^a=FALSE, b=TRUE, c=TRUE$ -^a=FALSE, b=FALSE, c=TRUE$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 6 iterations$ -- ^warning: ignoring From 9f1f0d9b9d0189089a34d640a339370ab25db163 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:24:16 +0100 Subject: [PATCH 10/15] fix test desc of mcdc9 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc9/test.desc | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc index ef0b713cafc..d8ec7ea5f82 100644 --- a/regression/cbmc-cover/mcdc9/test.desc +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -3,13 +3,12 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^A=TRUE, B=FALSE, C=TRUE, D=TRUE$ -^A=TRUE, B=FALSE, C=TRUE, D=FALSE$ -^A=TRUE, B=FALSE, C=FALSE, D=FALSE$ -^A=TRUE, B=FALSE, C=FALSE, D=TRUE$ -^A=FALSE, B=FALSE, C=FALSE, D=TRUE$ -^A=FALSE, B=TRUE, C=FALSE, D=FALSE$ -^A=FALSE, B=TRUE, C=TRUE, D=FALSE$ -^A=FALSE, B=FALSE, C=TRUE, D=FALSE$ +^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$ +^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && D != FALSE && A != FALSE && !(B != FALSE).* SATISFIED$ +^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE) && A != FALSE && !(B != FALSE).* SATISFIED$ +^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE && !(D != FALSE).* SATISFIED$ +^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 8 iterations$ -- ^warning: ignoring From 922ddc689a6ca45549c6ebaf45574d5765ff6c26 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:25:53 +0100 Subject: [PATCH 11/15] fix test desc of mcdc10 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc10/test.desc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc index 7df6b51ffac..daf502e74af 100644 --- a/regression/cbmc-cover/mcdc10/test.desc +++ b/regression/cbmc-cover/mcdc10/test.desc @@ -7,5 +7,7 @@ main.c ^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$ ^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$ ^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 5 iterations$ -- ^warning: ignoring From 47273c3c9d634fd484564778738937364749fe22 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:27:12 +0100 Subject: [PATCH 12/15] fix test desc of mcdc11 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc11/test.desc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc index 5a8585e1554..616b3249b0d 100644 --- a/regression/cbmc-cover/mcdc11/test.desc +++ b/regression/cbmc-cover/mcdc11/test.desc @@ -9,5 +9,7 @@ main.c ^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$ ^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$ ^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 6 iterations$ -- ^warning: ignoring From fc8a2187ab6586e9a7a71619db1c84f2785c8029 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:28:47 +0100 Subject: [PATCH 13/15] fix test desc of mcdc12 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc12/test.desc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc index 37779f1f821..44e823e13c4 100644 --- a/regression/cbmc-cover/mcdc12/test.desc +++ b/regression/cbmc-cover/mcdc12/test.desc @@ -12,5 +12,7 @@ main.c ^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !(F != FALSE).*: SATISFIED$ ^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && F != FALSE.*: SATISFIED$ ^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && !(F != FALSE).*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 10 iterations$ -- ^warning: ignoring From 91642a922430a130c1028e27e0b3021598bc41dc Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:30:55 +0100 Subject: [PATCH 14/15] fix test desc of mcdc13 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc13/main.c | 5 +++-- regression/cbmc-cover/mcdc13/test.desc | 10 ++++++---- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/regression/cbmc-cover/mcdc13/main.c b/regression/cbmc-cover/mcdc13/main.c index b26bef260cc..d875b00235f 100644 --- a/regression/cbmc-cover/mcdc13/main.c +++ b/regression/cbmc-cover/mcdc13/main.c @@ -1,11 +1,12 @@ int main() { - _Bool A, B; + _Bool A, B, C; __CPROVER_input("A", A); __CPROVER_input("B", B); + __CPROVER_input("C", C); - if (A && B) + if (A && B && C) { /* instructions */ } diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc index 3d99dd739ff..c7983f47aa9 100644 --- a/regression/cbmc-cover/mcdc13/test.desc +++ b/regression/cbmc-cover/mcdc13/test.desc @@ -3,9 +3,11 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^A=FALSE, B=TRUE$ -^A=FALSE, B=FALSE$ -^A=TRUE, B=FALSE$ -^A=TRUE, B=TRUE$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !(C != FALSE).* SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE.* SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE.* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 6 iterations$ -- ^warning: ignoring From 7421019894129e15751262d6165154a5e60a0a07 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 27 Oct 2016 14:44:29 +0100 Subject: [PATCH 15/15] fix test case mcdc14 Signed-off-by: Lucas Cordeiro --- regression/cbmc-cover/mcdc14/main.c | 10 +++------- regression/cbmc-cover/mcdc14/test.desc | 8 ++++---- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/regression/cbmc-cover/mcdc14/main.c b/regression/cbmc-cover/mcdc14/main.c index 496ddb0c70d..ebc094c78d5 100644 --- a/regression/cbmc-cover/mcdc14/main.c +++ b/regression/cbmc-cover/mcdc14/main.c @@ -1,14 +1,10 @@ int main() { - _Bool A, B, C; + int altitude; - __CPROVER_input("A", A); - __CPROVER_input("B", B); - __CPROVER_output("C", C); + __CPROVER_input("altitude", altitude); - C = (A || B); - - if (C) + if (altitude > 2500) { /* instructions */ } diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc index fc7c64c0396..6778dfcc2f8 100644 --- a/regression/cbmc-cover/mcdc14/test.desc +++ b/regression/cbmc-cover/mcdc14/test.desc @@ -3,9 +3,9 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^A=TRUE, B=FALSE$ -^A=TRUE, B=TRUE$ -^A=FALSE, B=TRUE$ -^A=FALSE, B=FALSE$ +^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ +^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 2 iterations$ -- ^warning: ignoring