Mark tests which fail due to invariant violations

There was an issue in cover.cpp where the begin() of an empty vector was
dereferenced. To avoid this case, we add an INVARIANT which checks that
the vector has at least one element. However, this causes some of the
tests to fail, so these have been marked KNOWNBUG.

Author: reuk

regression/cbmc-cover/built-ins7/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc --unwind 5
 ^EXIT=0$
@@ -7,3 +7,6 @@ main.c
 --
 ^warning: ignoring
 ^\[.*<builtin-library-
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc10/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc11/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc12/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -15,3 +15,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc13/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc14/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -9,3 +9,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc4/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc5/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc6/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc7/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc8/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc9/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

src/goto-instrument/cover.cpp

@@ -1553,10 +1553,8 @@ void instrument_cover_goals(
         remove_repetition(controlling);
         // for now, we restrict to the case of a single ''decision'';
         // however, this is not true, e.g., ''? :'' operator.
-        if(!decisions.empty())
-        {
-          minimize_mcdc_controlling(controlling, *decisions.begin());
-        }
+        INVARIANT(!decisions.empty(), "There must be at least one decision");
+        minimize_mcdc_controlling(controlling, *decisions.begin());
 
         for(const auto &p : controlling)
         {