Split ieee_floatt into ieee_float_valuet and ieee_floatt

diffblue · Dec 31, 2024 · f0d1f79 · f0d1f79
1 parent f9a7807
commit f0d1f79
Show file tree

Hide file tree

Showing 8 changed files with 331 additions and 305 deletions.
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -171,7 +171,8 @@ constant_exprt from_integer(
   }
   else if(type_id==ID_floatbv)
   {
-    ieee_floatt ieee_float(to_floatbv_type(type));
+    ieee_floatt ieee_float(to_floatbv_type(type), ieee_floatt::rounding_modet::ROUND_TO_EVEN);
+    // always rounds to zero
     ieee_float.from_integer(int_value);
     return ieee_float.to_expr();
   }

diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -75,7 +75,7 @@ bool exprt::is_zero() const
     }
     else if(type_id==ID_floatbv)
     {
-      if(ieee_floatt(constant)==0)
+      if(ieee_float_valuet(constant)==0)
         return true;
     }
     else if(type_id==ID_pointer)
@@ -131,7 +131,7 @@ bool exprt::is_one() const
     }
     else if(type_id==ID_floatbv)
     {
-      if(ieee_floatt(constant_expr) == 1)
+      if(ieee_float_valuet(constant_expr) == 1)
         return true;
     }
   }

diff --git a/src/util/format_constant.cpp b/src/util/format_constant.cpp
@@ -36,7 +36,7 @@ std::string format_constantt::operator()(const exprt &expr)
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      return ieee_floatt(to_constant_expr(expr)).format(*this);
+      return ieee_float_valuet(to_constant_expr(expr)).format(*this);
     }
   }
   else if(expr.id()==ID_string_constant)

diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
@@ -207,7 +207,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
   else if(type == ID_string)
     return os << '"' << escape(id2string(src.get_value())) << '"';
   else if(type == ID_floatbv)
-    return os << ieee_floatt(src);
+    return os << ieee_float_valuet(src);
   else if(type == ID_pointer)
   {
     if(src.is_null_pointer())