added model for FreeBSD __flt_rounds

Author: Daniel Kroening

src/ansi-c/library/float.c

@@ -83,3 +83,18 @@ inline int __builtin_flt_rounds(void)
          __CPROVER_rounding_mode==3?0: // to zero
          -1;
 }
+
+/* FUNCTION: __flt_rounds */
+
+extern int __CPROVER_rounding_mode;
+
+inline int __flt_rounds(void)
+{
+  // Spotted on FreeBSD
+  // See __builtin_flt_rounds for the magic numbers.
+  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;
+}