Introduce floatbv_rounding_mode(unsigned)

src/util/Makefile

@@ -22,6 +22,7 @@ SRC = allocate_objects.cpp \
       find_macros.cpp \
       find_symbols.cpp \
       fixedbv.cpp \
+      floatbv_expr.cpp \
       format_constant.cpp \
       format_expr.cpp \
       format_number_range.cpp \

src/util/floatbv_expr.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: API to expression classes for floating-point arithmetic
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "floatbv_expr.h"
+
+#include "arith_tools.h"
+#include "bitvector_types.h"
+
+constant_exprt floatbv_rounding_mode(unsigned rm)
+{
+  // The 32 bits are an arbitrary choice;
+  // e.g., float_utilst consumes other widths as well.
+  // The type is signed to match the signature of fesetround.
+  return ::from_integer(rm, signedbv_typet(32));
+}

src/util/floatbv_expr.h

@@ -438,4 +438,9 @@ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
   return ret;
 }
 
+/// \brief returns the a rounding mode expression for a given
+/// IEEE rounding mode, encoded using the recommendation in
+/// C11 5.2.4.2.2
+constant_exprt floatbv_rounding_mode(unsigned);
+
 #endif // CPROVER_UTIL_FLOATBV_EXPR_H

src/util/ieee_float.cpp

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "arith_tools.h"
 #include "bitvector_types.h"
-#include "c_types.h"
+#include "floatbv_expr.h"
 #include "invariant.h"
 #include "std_expr.h"
 
@@ -58,7 +58,7 @@ void ieee_float_spect::from_type(const floatbv_typet &type)
 
 constant_exprt ieee_floatt::rounding_mode_expr(rounding_modet rm)
 {
-  return ::from_integer(static_cast<int>(rm), unsigned_int_type());
+  return floatbv_rounding_mode(static_cast<unsigned>(rm));
 }
 
 void ieee_floatt::print(std::ostream &out) const

src/util/ieee_float.h

@@ -120,7 +120,8 @@ class ieee_floatt
 public:
   // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and
   // is the IEEE default.
-  // The numbering below is what x86 uses in the control word.
+  // The numbering below is what x86 uses in the control word and
+  // what is recommended in C11 5.2.4.2.2
   enum rounding_modet
   {
     ROUND_TO_EVEN=0, ROUND_TO_MINUS_INF=1,