C library: implement feraiseexcept

Model floating-point exceptions as failing assertions.

Author: tautschnig

regression/cbmc-library/feraiseexcept-01/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <fenv.h>
+
+int main()
+{
+  int exceptions;
+  feraiseexcept(exceptions);
+  return 0;
+}

regression/cbmc-library/feraiseexcept-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/library/fenv.c

@@ -40,3 +40,12 @@ __CPROVER_HIDE:;
     0;
   return 0; // we never fail
 }
+
+/* FUNCTION: feraiseexcept */
+
+int feraiseexcept(int excepts)
+{
+__CPROVER_HIDE:;
+  __CPROVER_assert(excepts == 0, "floating-point exception");
+  return 0; // we never fail
+}