add test cases related to boundary values by Youcheng

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>

regression/cbmc-cover/mcdc-boundary-values1/main.c

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

regression/cbmc-cover/mcdc-boundary-values1/test.desc

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

regression/cbmc-cover/mcdc-boundary-values2/main.c

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

regression/cbmc-cover/mcdc-boundary-values2/test.desc

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

regression/cbmc-cover/mcdc-boundary-values3/main.c

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

regression/cbmc-cover/mcdc-boundary-values3/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover boundary-values
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 7 function main MC/DC independence condition `altitude > 2500.* SATISFIED$
+^\[main.coverage.2\] file main.c line 7 function main MC/DC independence condition `altitude == 2500.* SATISFIED$
+^\[main.coverage.3\] file main.c line 7 function main MC/DC independence condition `altitude < 2500.* SATISFIED$
+^\[main.coverage.4\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
+^\[main.coverage.5\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 3 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc-boundary-values4/main.c

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

regression/cbmc-cover/mcdc-boundary-values4/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover boundary-values
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `A != FALSE.* SATISFIED$
+^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `A == FALSE.* SATISFIED$
+^\[main.coverage.3\] file main.c line 8 function main decision/condition `A != FALSE.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 8 function main decision/condition `A != FALSE.* SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 2 iterations$
+--
+^warning: ignoring