Merge pull request #8550 from diffblue/ieee_float_valuet

kroening · web-flow · commit af4e2e4f10b6 · 2025-02-04T22:03:22.000Z
Split `ieee_floatt` into `ieee_float_valuet` and `ieee_floatt`
diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -358,13 +358,13 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)
   }
   else if(expr.type() == java_double_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_double(std::stod(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
   else if(expr.type() == java_float_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_float(std::stof(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
@@ -230,7 +230,7 @@ std::string expr2javat::convert_constant(
           (src.type()==java_double_type()))
   {
     // This converts NaNs to the canonical NaN
-    const ieee_floatt ieee_repr(to_constant_expr(src));
+    const ieee_float_valuet ieee_repr(to_constant_expr(src));
     if(ieee_repr.is_double())
       return floating_point_to_java_string(ieee_repr.to_double());
     return floating_point_to_java_string(ieee_repr.to_float());
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2181,16 +2181,19 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
       is_float ? ieee_float_spect::single_precision()
                : ieee_float_spect::double_precision());
 
-    ieee_floatt value(spec);
     if(arg0.type().id() != ID_floatbv)
     {
+      // conversion from integer to float may need rounding
+      auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
       const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      ieee_floatt value(spec, rm);
       value.from_integer(number);
+      results[0] = value.to_expr();
     }
     else
-      value.from_expr(arg0);
-
-    results[0] = value.to_expr();
+    {
+      results[0] = ieee_float_valuet{arg0}.to_expr();
+    }
   }
   else
   {
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -782,7 +782,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Float:
       {
-        ieee_floatt value(ieee_float_spect::single_precision());
+        ieee_float_valuet value(ieee_float_spect::single_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }
@@ -794,7 +794,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Double:
       {
-        ieee_floatt value(ieee_float_spect::double_precision());
+        ieee_float_valuet value(ieee_float_spect::double_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -938,7 +938,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Expression representing 0.0
   const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
-  ieee_floatt zero_float(float_spec);
+  ieee_float_valuet zero_float(float_spec);
   zero_float.from_float(0.0);
   const constant_exprt zero = zero_float.to_expr();
 
@@ -996,16 +996,17 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   string_expr_list.push_back(zero_string);
 
   // Case of -0.0
-  ieee_floatt minus_zero_float(float_spec);
+  ieee_float_valuet minus_zero_float(float_spec);
   minus_zero_float.from_float(-0.0f);
   condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
   const refined_string_exprt minus_zero_string =
     string_literal_to_string_expr("-0.0", loc, symbol_table, code);
   string_expr_list.push_back(minus_zero_string);
 
   // Case of simple notation
-  ieee_floatt bound_inf_float(float_spec);
-  ieee_floatt bound_sup_float(float_spec);
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt bound_inf_float(float_spec, rm);
+  ieee_floatt bound_sup_float(float_spec, rm);
   bound_inf_float.from_float(1e-3f);
   bound_sup_float.from_float(1e7f);
   bound_inf_float.change_spec(float_spec);
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
@@ -288,7 +288,7 @@ void interval_domaint::assume_rec(
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(rhs));
+      ieee_float_valuet tmp(to_constant_expr(rhs));
       if(id==ID_lt)
         tmp.decrement();
       ieee_float_intervalt &fi=float_map[lhs_identifier];
@@ -313,7 +313,7 @@ void interval_domaint::assume_rec(
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(lhs));
+      ieee_float_valuet tmp(to_constant_expr(lhs));
       if(id==ID_lt)
         tmp.increment();
       ieee_float_intervalt &fi=float_map[rhs_identifier];
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ai_domain.h"
 
-typedef interval_templatet<ieee_floatt> ieee_float_intervalt;
+typedef interval_templatet<ieee_float_valuet> ieee_float_intervalt;
 
 class interval_domaint:public ai_domain_baset
 {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1912,7 +1912,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_floatbv)
   {
-    dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();
+    dest = ieee_float_valuet(to_constant_expr(src)).to_ansi_c_string();
 
     if(!dest.empty() && isdigit(dest[dest.size() - 1]))
     {
diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -761,12 +761,13 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       else if(old_type.id() == ID_floatbv) // float -> signed
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width - 1));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-power(2, new_width - 1) - 1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -844,12 +845,13 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       else if(old_type.id() == ID_floatbv) // float -> unsigned
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -1295,8 +1297,8 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
     // -inf + +inf = NaN and +inf + -inf = NaN,
     // i.e., signs differ
     ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(
@@ -1315,8 +1317,8 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
 
     ieee_float_spect spec =
       ieee_float_spect(to_floatbv_type(minus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(
diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
@@ -71,7 +71,9 @@ exprt convert_float_literal(const std::string &src)
     // but these aren't handled anywhere
   }
 
-  ieee_floatt a(type);
+  // This may require rounding.
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt a(type, rm);
 
   if(parsed_float.exponent_base==10)
     a.from_base10(parsed_float.significand, parsed_float.exponent);
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -1923,7 +1923,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
   {
     if(expr.type().id()==ID_floatbv)
     {
-      const ieee_floatt f(to_constant_expr(expr));
+      const ieee_float_valuet f(to_constant_expr(expr));
       if(f.is_NaN() || f.is_infinity())
         system_headers.insert("math.h");
     }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -576,7 +576,7 @@ exprt interpretert::get_value(
   }
   else if(type.id() == ID_floatbv)
   {
-    ieee_floatt f(to_floatbv_type(type));
+    ieee_float_valuet f(to_floatbv_type(type));
     f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
     return f.to_expr();
   }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -364,7 +364,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      ieee_floatt f;
+      ieee_float_valuet f;
       f.from_expr(to_constant_expr(expr));
       return {f.pack()};
     }
@@ -731,8 +731,9 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
         }
         else if(expr.type().id()==ID_floatbv)
         {
-          ieee_floatt f1(to_floatbv_type(expr.type()));
-          ieee_floatt f2(to_floatbv_type(op.type()));
+          auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+          ieee_floatt f1(to_floatbv_type(expr.type()), rm);
+          ieee_floatt f2(to_floatbv_type(op.type()), rm);
           f1.unpack(result);
           f2.unpack(tmp.front());
           f1*=f2;
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
@@ -276,7 +276,7 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
         json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
       result["data"] =
-        json_stringt(ieee_floatt(constant_expr).to_ansi_c_string());
+        json_stringt(ieee_float_valuet(constant_expr).to_ansi_c_string());
     }
     else if(type.id() == ID_pointer)
     {
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
@@ -212,7 +212,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       result.set_attribute("width", width);
       result.set_attribute(
         "binary", integer2binary(bvrep2integer(value, width, false), width));
-      result.data = ieee_floatt(constant_expr).to_ansi_c_string();
+      result.data = ieee_float_valuet(constant_expr).to_ansi_c_string();
     }
     else if(type.id() == ID_pointer)
     {
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
@@ -240,7 +240,7 @@ exprt float_bvt::is_zero(const exprt &src)
 
   constant_exprt mask(integer2bvrep(v, width), src.type());
 
-  ieee_floatt z(type);
+  ieee_float_valuet z(type);
   z.make_zero();
 
   return equal_exprt(bitand_exprt(src, mask), z.to_expr());
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
@@ -136,7 +136,7 @@ bvt float_utilst::to_integer(
   return result;
 }
 
-bvt float_utilst::build_constant(const ieee_floatt &src)
+bvt float_utilst::build_constant(const ieee_float_valuet &src)
 {
   unbiased_floatt result;
 
@@ -1268,14 +1268,14 @@ bvt float_utilst::pack(const biased_floatt &src)
   return result;
 }
 
-ieee_floatt float_utilst::get(const bvt &src) const
+ieee_float_valuet float_utilst::get(const bvt &src) const
 {
   mp_integer int_value=0;
 
   for(std::size_t i=0; i<src.size(); i++)
     int_value+=power(2, i)*prop.l_get(src[i]).is_true();
 
-  ieee_floatt result;
+  ieee_float_valuet result;
   result.spec=spec;
   result.unpack(int_value);
 
diff --git a/src/solvers/floatbv/float_utils.h b/src/solvers/floatbv/float_utils.h
@@ -87,7 +87,7 @@ class float_utilst
 
   ieee_float_spect spec;
 
-  bvt build_constant(const ieee_floatt &);
+  bvt build_constant(const ieee_float_valuet &);
 
   static inline literalt sign_bit(const bvt &src)
   {
@@ -139,7 +139,7 @@ class float_utilst
   literalt relation(const bvt &src1, relt rel, const bvt &src2);
 
   // constants
-  ieee_floatt get(const bvt &) const;
+  ieee_float_valuet get(const bvt &) const;
 
   // helpers
   literalt exponent_all_ones(const bvt &);
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -476,23 +476,25 @@ constant_exprt smt2_convt::parse_literal(
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::plus_infinity(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::plus_infinity(ieee_float_spect(s - 1, e))
+      .to_expr();
   }
   else if(src.get_sub().size()==4 &&
           src.get_sub()[0].id()=="_" &&
           src.get_sub()[1].id()=="-oo") // (_ -oo e s)
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::minus_infinity(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::minus_infinity(ieee_float_spect(s - 1, e))
+      .to_expr();
   }
   else if(src.get_sub().size()==4 &&
           src.get_sub()[0].id()=="_" &&
           src.get_sub()[1].id()=="NaN") // (_ NaN e s)
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::NaN(ieee_float_spect(s - 1, e)).to_expr();
   }
 
   if(type.id()==ID_signedbv ||
@@ -3457,7 +3459,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
          significands including the hidden bit.  Thus some encoding
          is needed to get to IEEE-754 style representations. */
 
-      ieee_floatt v=ieee_floatt(expr);
+      ieee_float_valuet v = ieee_float_valuet(expr);
       size_t e=floatbv_type.get_e();
       size_t f=floatbv_type.get_f()+1;
 
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
@@ -93,7 +93,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     }
     else if(expr_type.id() == ID_floatbv)
     {
-      const ieee_floatt v = ieee_floatt(constant_expr);
+      const ieee_float_valuet v = ieee_float_valuet(constant_expr);
       const size_t e = v.spec.e;
       const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit
 
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
@@ -77,7 +77,7 @@ exprt get_significand(
 /// \return an expression representing this floating point
 exprt constant_float(const double f, const ieee_float_spect &float_spec)
 {
-  ieee_floatt fl(float_spec);
+  ieee_float_valuet fl(float_spec);
   if(float_spec == ieee_float_spect::single_precision())
     fl.from_float(f);
   else if(float_spec == ieee_float_spect::double_precision())
diff --git a/src/statement-list/converters/convert_real_literal.cpp b/src/statement-list/converters/convert_real_literal.cpp
@@ -18,7 +18,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 
 constant_exprt convert_real_literal(const std::string &src)
 {
-  ieee_floatt real{get_real_type()};
+  ieee_float_valuet real{get_real_type()};
   real.from_float(std::stof(src));
   return real.to_expr();
 }
diff --git a/src/statement-list/statement_list_parse_tree_io.cpp b/src/statement-list/statement_list_parse_tree_io.cpp
@@ -31,7 +31,7 @@ static void output_constant(std::ostream &os, const constant_exprt &constant)
     os << ivalue;
   else if(can_cast_type<floatbv_typet>(constant.type()))
   {
-    ieee_floatt real{get_real_type()};
+    ieee_float_valuet real{get_real_type()};
     real.from_expr(constant);
     os << real.to_float();
   }
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -171,7 +171,9 @@ 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
diff --git a/src/util/format_constant.cpp b/src/util/format_constant.cpp
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
diff --git a/unit/solvers/floatbv/float_utils.cpp b/unit/solvers/floatbv/float_utils.cpp

Original file line number	Diff line number	Diff line change
`@@ -358,13 +358,13 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)`
`358`	`358`	`}`
`359`	`359`	`else if(expr.type() == java_double_type())`
`360`	`360`	`{`
`361`		`- ieee_floatt ieee_float(to_floatbv_type(expr.type()));`
	`361`	`+ ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));`
`362`	`362`	`ieee_float.from_double(std::stod(json.value));`
`363`	`363`	`result.add(code_frontend_assignt{expr, ieee_float.to_expr()});`
`364`	`364`	`}`
`365`	`365`	`else if(expr.type() == java_float_type())`
`366`	`366`	`{`
`367`		`- ieee_floatt ieee_float(to_floatbv_type(expr.type()));`
	`367`	`+ ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));`
`368`	`368`	`ieee_float.from_float(std::stof(json.value));`
`369`	`369`	`result.add(code_frontend_assignt{expr, ieee_float.to_expr()});`
`370`	`370`	`}`
Original file line number	Diff line number	Diff line change
`@@ -230,7 +230,7 @@ std::string expr2javat::convert_constant(`
`230`	`230`	`(src.type()==java_double_type()))`
`231`	`231`	`{`
`232`	`232`	`// This converts NaNs to the canonical NaN`
`233`		`- const ieee_floatt ieee_repr(to_constant_expr(src));`
	`233`	`+ const ieee_float_valuet ieee_repr(to_constant_expr(src));`
`234`	`234`	`if(ieee_repr.is_double())`
`235`	`235`	`return floating_point_to_java_string(ieee_repr.to_double());`
`236`	`236`	`return floating_point_to_java_string(ieee_repr.to_float());`
Original file line number	Diff line number	Diff line change
`@@ -2181,16 +2181,19 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(`
`2181`	`2181`	`is_float ? ieee_float_spect::single_precision()`
`2182`	`2182`	`: ieee_float_spect::double_precision());`
`2183`	`2183`
`2184`		`- ieee_floatt value(spec);`
`2185`	`2184`	`if(arg0.type().id() != ID_floatbv)`
`2186`	`2185`	`{`
	`2186`	`+ // conversion from integer to float may need rounding`
	`2187`	`+ auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;`
`2187`	`2188`	`const mp_integer number = numeric_cast_v<mp_integer>(arg0);`
	`2189`	`+ ieee_floatt value(spec, rm);`
`2188`	`2190`	`value.from_integer(number);`
	`2191`	`+ results[0] = value.to_expr();`
`2189`	`2192`	`}`
`2190`	`2193`	`else`
`2191`		`- value.from_expr(arg0);`
`2192`		`-`
`2193`		`- results[0] = value.to_expr();`
	`2194`	`+ {`
	`2195`	`+ results[0] = ieee_float_valuet{arg0}.to_expr();`
	`2196`	`+ }`
`2194`	`2197`	`}`
`2195`	`2198`	`else`
`2196`	`2199`	`{`
Original file line number	Diff line number	Diff line change
`@@ -782,7 +782,7 @@ void java_bytecode_parsert::rconstant_pool()`
`782`	`782`
`783`	`783`	`case CONSTANT_Float:`
`784`	`784`	`{`
`785`		`- ieee_floatt value(ieee_float_spect::single_precision());`
	`785`	`+ ieee_float_valuet value(ieee_float_spect::single_precision());`
`786`	`786`	`value.unpack(entry.number);`
`787`	`787`	`entry.expr = value.to_expr();`
`788`	`788`	`}`
`@@ -794,7 +794,7 @@ void java_bytecode_parsert::rconstant_pool()`
`794`	`794`
`795`	`795`	`case CONSTANT_Double:`
`796`	`796`	`{`
`797`		`- ieee_floatt value(ieee_float_spect::double_precision());`
	`797`	`+ ieee_float_valuet value(ieee_float_spect::double_precision());`
`798`	`798`	`value.unpack(entry.number);`
`799`	`799`	`entry.expr = value.to_expr();`
`800`	`800`	`}`
Original file line number	Diff line number	Diff line change
`@@ -288,7 +288,7 @@ void interval_domaint::assume_rec(`
`288`	`288`	`}`
`289`	`289`	`else if(is_float(lhs.type()) && is_float(rhs.type()))`
`290`	`290`	`{`
`291`		`- ieee_floatt tmp(to_constant_expr(rhs));`
	`291`	`+ ieee_float_valuet tmp(to_constant_expr(rhs));`
`292`	`292`	`if(id==ID_lt)`
`293`	`293`	`tmp.decrement();`
`294`	`294`	`ieee_float_intervalt &fi=float_map[lhs_identifier];`
`@@ -313,7 +313,7 @@ void interval_domaint::assume_rec(`
`313`	`313`	`}`
`314`	`314`	`else if(is_float(lhs.type()) && is_float(rhs.type()))`
`315`	`315`	`{`
`316`		`- ieee_floatt tmp(to_constant_expr(lhs));`
	`316`	`+ ieee_float_valuet tmp(to_constant_expr(lhs));`
`317`	`317`	`if(id==ID_lt)`
`318`	`318`	`tmp.increment();`
`319`	`319`	`ieee_float_intervalt &fi=float_map[rhs_identifier];`
Original file line number	Diff line number	Diff line change
`@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]`
`18`	`18`
`19`	`19`	`#include "ai_domain.h"`
`20`	`20`
`21`		`-typedef interval_templatet<ieee_floatt> ieee_float_intervalt;`
	`21`	`+typedef interval_templatet<ieee_float_valuet> ieee_float_intervalt;`
`22`	`22`
`23`	`23`	`class interval_domaint:public ai_domain_baset`
`24`	`24`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1912,7 +1912,7 @@ std::string expr2ct::convert_constant(`
`1912`	`1912`	`}`
`1913`	`1913`	`else if(type.id()==ID_floatbv)`
`1914`	`1914`	`{`
`1915`		`- dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();`
	`1915`	`+ dest = ieee_float_valuet(to_constant_expr(src)).to_ansi_c_string();`
`1916`	`1916`
`1917`	`1917`	`if(!dest.empty() && isdigit(dest[dest.size() - 1]))`
`1918`	`1918`	`{`
Original file line number	Diff line number	Diff line change
`@@ -71,7 +71,9 @@ exprt convert_float_literal(const std::string &src)`
`71`	`71`	`// but these aren't handled anywhere`
`72`	`72`	`}`
`73`	`73`
`74`		`- ieee_floatt a(type);`
	`74`	`+ // This may require rounding.`
	`75`	`+ auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;`
	`76`	`+ ieee_floatt a(type, rm);`
`75`	`77`
`76`	`78`	`if(parsed_float.exponent_base==10)`
`77`	`79`	`a.from_base10(parsed_float.significand, parsed_float.exponent);`