Boundary value analysis (do not merge)

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 mcdc --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 mcdc --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 mcdc --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 mcdc --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

regression/cbmc-cover/mcdc1/test.desc

@@ -3,12 +3,11 @@ 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.1\] file main.c line 14 function main MC/DC independence condition `A && !B && C && D && !E.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `A && !B && C && !D && E.*: SATISFIED$
+^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `A && !B && !C && D && E.*: 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 10 iterations$
 --

regression/cbmc-cover/mcdc8/test.desc

@@ -3,10 +3,10 @@ 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$
+^\[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$
 --

src/cbmc/Makefile

@@ -22,6 +22,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
+      ../goto-instrument/cover_utils$(OBJEXT) \
+      ../goto-instrument/cover_mcdc$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \

src/cbmc/cbmc_parse_options.cpp

@@ -930,6 +930,8 @@ bool cbmc_parse_optionst::process_goto_program(
           c=coverage_criteriont::MCDC;
         else if(criterion_string=="cover")
           c=coverage_criteriont::COVER;
+        else if(criterion_string=="boundary-values")
+          c=coverage_criteriont::BOUNDARY;
         else
         {
           error() << "unknown coverage criterion" << eom;
@@ -941,8 +943,8 @@ bool cbmc_parse_optionst::process_goto_program(
 
       status() << "Instrumenting coverage goals" << eom;
 
-      for(const auto & criterion : criteria)
-        instrument_cover_goals(symbol_table, goto_functions, criterion);
+      instrument_cover_goalst goals(symbol_table, criteria);
+      goals.instrument_cover_goals(goto_functions);
 
       goto_functions.update();
     }

src/goto-instrument/Makefile

@@ -23,7 +23,7 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \
       wmm/event_graph.cpp wmm/pair_collection.cpp \
       goto_instrument_main.cpp horn_encoding.cpp \
       thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \
-      code_contracts.cpp cover.cpp
+      code_contracts.cpp cover_utils.cpp cover_mcdc.cpp cover.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \