Mark tests which fail due to invariant violations

reuk · reuk · commit d423c65705b8 · 2017-11-27T14:09:39.000Z
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.
diff --git a/regression/cbmc-cover/built-ins7/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc1/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc10/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc11/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc12/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc13/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc14/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc2/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc3/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc4/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc5/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc6/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc7/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc8/test.desc b/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
diff --git a/regression/cbmc-cover/mcdc9/test.desc b/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
diff --git a/src/goto-instrument/cover.cpp b/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)
         {
