support clang's __builtin_flt_rounds

Author: Daniel Kroening

regression/cbmc/Float-Rounding3/main.c

@@ -0,0 +1,31 @@
+// This is C99, but currently only works with clang.
+// gcc and Visual Studio appear to hard-wire FLT_ROUNDS to 1.
+
+#ifdef __clang__
+
+#include <assert.h>
+#include <fenv.h>
+#include <float.h>
+
+int main()
+{
+  fesetround(FE_DOWNWARD);
+  assert(FLT_ROUNDS==3);
+
+  fesetround(FE_TONEAREST);
+  assert(FLT_ROUNDS==1);
+
+  fesetround(FE_TOWARDZERO);
+  assert(FLT_ROUNDS==0);
+
+  fesetround(FE_UPWARD);
+  assert(FLT_ROUNDS==2);
+}
+
+#else
+
+int main()
+{
+}
+
+#endif

regression/cbmc/Float-Rounding3/test.desc

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

src/ansi-c/clang_builtin_headers.h

@@ -1,3 +1,5 @@
 typedef float  __gcc_v4sf  __attribute__ ((__vector_size__ (16)));
 
 __gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...);
+
+int __builtin_flt_rounds(void);

src/ansi-c/library/float.c

@@ -67,3 +67,19 @@ inline int _isnan(double x)
 {
   return __CPROVER_isnand(x);
 }
+
+/* FUNCTION: __builtin_flt_rounds */
+
+extern int __CPROVER_rounding_mode;
+
+inline int __builtin_flt_rounds(void)
+{
+  // This is a clang builtin for FLT_ROUNDS
+  // The magic numbers are C99 and different from the
+  // x86 encoding that CPROVER uses.
+  return __CPROVER_rounding_mode==0?1: // to nearest
+         __CPROVER_rounding_mode==1?3: // downward
+         __CPROVER_rounding_mode==2?2: // upward
+         __CPROVER_rounding_mode==3?0: // to zero
+         -1;
+}