Revert "Mark tests which fail due to invariant violations"

This reverts commit d423c65.
NathanJPhillips · Jul 9, 2018 · 15f44c7 · 15f44c7
1 parent 0d7a943
commit 15f44c7
Show file tree

Hide file tree

Showing 16 changed files with 19 additions and 62 deletions.
diff --git a/regression/cbmc-cover/built-ins7/test.desc b/regression/cbmc-cover/built-ins7/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc --unwind 5
 ^EXIT=0$
@@ -7,6 +7,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,6 +12,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,6 +10,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,6 +12,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -15,6 +15,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,6 +10,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,6 +8,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,6 +10,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -9,6 +9,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,6 +11,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,6 +11,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,6 +8,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,6 +10,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,6 +10,3 @@ 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 @@
-KNOWNBUG
+CORE
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,6 +11,3 @@ 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_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp
@@ -706,8 +706,10 @@ void cover_mcdc_instrumentert::instrument(
     remove_repetition(controlling);
     // for now, we restrict to the case of a single ''decision'';
     // however, this is not true, e.g., ''? :'' operator.
-    INVARIANT(!decisions.empty(), "There must be at least one decision");
-    minimize_mcdc_controlling(controlling, *decisions.begin());
+    if(!decisions.empty())
+    {
+      minimize_mcdc_controlling(controlling, *decisions.begin());
+    }
 
     for(const auto &p : controlling)
     {