Improved MCDC coverage

regression/cbmc-cover/mcdc1/main.c

@@ -17,4 +17,6 @@ int main()
   else
   {
   }
+
+  return 1;
 }

regression/cbmc-cover/mcdc1/test.desc

@@ -3,7 +3,13 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
+^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
+^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
+^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
 ^\*\* .* of .* covered (100.0%)$
-^\*\* Used 6 iterations$
+^\*\* Used 10 iterations$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc2/main.c

@@ -0,0 +1,18 @@
+int main()
+{
+
+  __CPROVER_bool A, B, C;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+
+  if(A||B||C)
+  {
+  }
+  else
+  {
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc2/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 && !B && !C.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
+^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc3/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  unsigned x, y;
+  if (!(x>3) && y<5) 
+    ;
+
+  return 1;
+}

regression/cbmc-cover/mcdc3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
+^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 4 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc4/main.c

@@ -0,0 +1,19 @@
+int main()
+{
+
+  __CPROVER_bool A, B, C, D;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+
+  if((A && B) || (C && D)) 
+  {
+  }
+  else
+  {
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc4/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
+^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
+^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 9 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc5/main.c

@@ -0,0 +1,18 @@
+int main()
+{
+  __CPROVER_bool A, B, C, D;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+
+  if((A || B)  && (C || D)) 
+  {
+  }
+  else
+  {
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc5/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
+^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
+^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 9 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc6/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  unsigned x;
+  if(x<3) 
+    ;
+
+  return 1;
+}

regression/cbmc-cover/mcdc6/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
+^\[main.coverage.2\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 2 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc7/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  signed x, y;
+
+  y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 );
+
+  return 1;
+}

regression/cbmc-cover/mcdc7/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 5 function main decision/condition `x \* 123 > 100.* false: SATISFIED$
+^\[main.coverage.2\] file main.c line 5 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
+^\[main.coverage.3\] file main.c line 5 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
+^\[main.coverage.4\] file main.c line 5 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 2 iterations$
+--
+^warning: ignoring