Merge pull request #700 from lucasccordeiro/fix-full-slice-04

Enabled test cases in goto-instrument after fixes in the full-slice

Author: Daniel Kroening

regression/goto-instrument/slice01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---unwind 2 --full-slice
+--unwind 2 --full-slice --add-library
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice13/main.c

@@ -17,7 +17,9 @@ void test (int mode, double d, float result) {
 
 int main (void)
 {
+#ifdef __GNUC__
   // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
   test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
+#endif
   return 1;
 }

regression/goto-instrument/slice13/test.desc

@@ -1,8 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---floatbv --full-slice
+--full-slice --add-library
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring

regression/goto-instrument/slice16/test.desc

@@ -1,8 +1,6 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice --unwind 2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring