From d1a7403fbfb3205704cc12ac0367a1c3e552cb57 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 9 Aug 2017 13:46:32 +0200
Subject: [PATCH] support clang's __builtin_flt_rounds

---
 regression/cbmc/Float-Rounding3/main.c    | 31 +++++++++++++++++++++++
 regression/cbmc/Float-Rounding3/test.desc |  8 ++++++
 src/ansi-c/clang_builtin_headers.h        |  2 ++
 src/ansi-c/library/float.c                | 16 ++++++++++++
 4 files changed, 57 insertions(+)
 create mode 100644 regression/cbmc/Float-Rounding3/main.c
 create mode 100644 regression/cbmc/Float-Rounding3/test.desc

diff --git a/regression/cbmc/Float-Rounding3/main.c b/regression/cbmc/Float-Rounding3/main.c
new file mode 100644
index 0000000000..bc4062b91f
--- /dev/null
+++ b/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
diff --git a/regression/cbmc/Float-Rounding3/test.desc b/regression/cbmc/Float-Rounding3/test.desc
new file mode 100644
index 0000000000..9efefbc736
--- /dev/null
+++ b/regression/cbmc/Float-Rounding3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/clang_builtin_headers.h b/src/ansi-c/clang_builtin_headers.h
index 9d266dda42..742cba71db 100644
--- a/src/ansi-c/clang_builtin_headers.h
+++ b/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);
diff --git a/src/ansi-c/library/float.c b/src/ansi-c/library/float.c
index ef82057ab4..204ad8d962 100644
--- a/src/ansi-c/library/float.c
+++ b/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;
+}