Siemens fix258

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;
+}

regression/cbmc-cover/mcdc10/test.desc

@@ -0,0 +1,13 @@
+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$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 5 iterations$
+--
+^warning: ignoring

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;
+}

regression/cbmc-cover/mcdc11/test.desc

@@ -0,0 +1,15 @@
+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$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring

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;
+}

regression/cbmc-cover/mcdc12/test.desc

@@ -0,0 +1,18 @@
+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$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 10 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc13/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  _Bool A, B, C;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+
+  if (A && B && C)
+  {
+    /* instructions */
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc13/test.desc

@@ -0,0 +1,13 @@
+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$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc14/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int altitude;
+
+  __CPROVER_input("altitude", altitude);
+
+  if (altitude > 2500)
+  {
+    /* instructions */  
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc14/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[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

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;
+}

regression/cbmc-cover/mcdc8/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[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

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;
+}

regression/cbmc-cover/mcdc9/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[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