use constructor for constant_exprt in convert_float_literal

src/ansi-c/gcc_types.cpp

@@ -11,15 +11,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/c_types.h>
 
-bitvector_typet gcc_float16_type()
+floatbv_typet gcc_float16_type()
 {
   floatbv_typet result=
     ieee_float_spect::half_precision().to_type();
   result.set(ID_C_c_type, ID_gcc_float16);
   return result;
 }
 
-bitvector_typet gcc_float32_type()
+floatbv_typet gcc_float32_type()
 {
   // not same as float!
   floatbv_typet result=
@@ -28,7 +28,7 @@ bitvector_typet gcc_float32_type()
   return result;
 }
 
-bitvector_typet gcc_float32x_type()
+floatbv_typet gcc_float32x_type()
 {
   // not same as float!
   floatbv_typet result=
@@ -37,7 +37,7 @@ bitvector_typet gcc_float32x_type()
   return result;
 }
 
-bitvector_typet gcc_float64_type()
+floatbv_typet gcc_float64_type()
 {
   // not same as double!
   floatbv_typet result=
@@ -46,7 +46,7 @@ bitvector_typet gcc_float64_type()
   return result;
 }
 
-bitvector_typet gcc_float64x_type()
+floatbv_typet gcc_float64x_type()
 {
   // not same as double!
   floatbv_typet result=
@@ -55,7 +55,7 @@ bitvector_typet gcc_float64x_type()
   return result;
 }
 
-bitvector_typet gcc_float128_type()
+floatbv_typet gcc_float128_type()
 {
   // not same as long double!
   floatbv_typet result=
@@ -64,7 +64,7 @@ bitvector_typet gcc_float128_type()
   return result;
 }
 
-bitvector_typet gcc_float128x_type()
+floatbv_typet gcc_float128x_type()
 {
   // not same as long double!
   floatbv_typet result=

src/ansi-c/gcc_types.h

@@ -14,13 +14,13 @@ Author: Daniel Kroening, [email protected]
 // These are gcc-specific; most are not implemented by clang
 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
 
-bitvector_typet gcc_float16_type();
-bitvector_typet gcc_float32_type();
-bitvector_typet gcc_float32x_type();
-bitvector_typet gcc_float64_type();
-bitvector_typet gcc_float64x_type();
-bitvector_typet gcc_float128_type();
-bitvector_typet gcc_float128x_type();
+floatbv_typet gcc_float16_type();
+floatbv_typet gcc_float32_type();
+floatbv_typet gcc_float32x_type();
+floatbv_typet gcc_float64_type();
+floatbv_typet gcc_float64x_type();
+floatbv_typet gcc_float128_type();
+floatbv_typet gcc_float128x_type();
 unsignedbv_typet gcc_unsigned_int128_type();
 signedbv_typet gcc_signed_int128_type();
 

src/ansi-c/literals/convert_float_literal.cpp

@@ -25,48 +25,49 @@ Author: Daniel Kroening, [email protected]
 
 #include "parse_float.h"
 
+/// build an expression from a floating-point literal
+/// \returns either a constant_exprt or a complex_exprt
 exprt convert_float_literal(const std::string &src)
 {
   parse_floatt parsed_float(src);
 
-  exprt result=exprt(ID_constant);
-
   // In ANSI-C, float literals are double by default,
-  // unless marked with 'f'.
-  // All of these can be complex as well.
-  // This can be overridden with
-  // config.ansi_c.single_precision_constant.
+  // unless marked with 'f' (this can be overridden with
+  // config.ansi_c.single_precision_constant).
+  // Furthermore, floating-point literals can be complex.
+
+  floatbv_typet type;
 
   if(parsed_float.is_float)
-    result.type()=float_type();
+    type = float_type();
   else if(parsed_float.is_long)
-    result.type()=long_double_type();
+    type = long_double_type();
   else if(parsed_float.is_float16)
-    result.type()=gcc_float16_type();
+    type = gcc_float16_type();
   else if(parsed_float.is_float32)
-    result.type()=gcc_float32_type();
+    type = gcc_float32_type();
   else if(parsed_float.is_float32x)
-    result.type()=gcc_float32x_type();
+    type = gcc_float32x_type();
   else if(parsed_float.is_float64)
-    result.type()=gcc_float64_type();
+    type = gcc_float64_type();
   else if(parsed_float.is_float64x)
-    result.type()=gcc_float64x_type();
+    type = gcc_float64x_type();
   else if(parsed_float.is_float80)
   {
-    result.type()=ieee_float_spect(64, 15).to_type();
-    result.type().set(ID_C_c_type, ID_long_double);
+    type = ieee_float_spect(64, 15).to_type();
+    type.set(ID_C_c_type, ID_long_double);
   }
   else if(parsed_float.is_float128)
-    result.type()=gcc_float128_type();
+    type = gcc_float128_type();
   else if(parsed_float.is_float128x)
-    result.type()=gcc_float128x_type();
+    type = gcc_float128x_type();
   else
   {
     // default
     if(config.ansi_c.single_precision_constant)
-      result.type()=float_type(); // default
+      type = float_type(); // default
     else
-      result.type()=double_type(); // default
+      type = double_type(); // default
   }
 
   if(parsed_float.is_decimal)
@@ -75,7 +76,7 @@ exprt convert_float_literal(const std::string &src)
     // but these aren't handled anywhere
   }
 
-  ieee_floatt a(to_floatbv_type(result.type()));
+  ieee_floatt a(type);
 
   if(parsed_float.exponent_base==10)
     a.from_base10(parsed_float.significand, parsed_float.exponent);
@@ -84,14 +85,12 @@ exprt convert_float_literal(const std::string &src)
   else
     UNREACHABLE;
 
-  result.set(
-    ID_value,
-    integer2binary(a.pack(), a.spec.width()));
+  constant_exprt result(integer2bv(a.pack(), a.spec.width()), type);
 
   if(parsed_float.is_imaginary)
   {
-    const complex_typet complex_type(result.type());
-    return complex_exprt(from_integer(0, result.type()), result, complex_type);
+    const complex_typet complex_type(type);
+    return complex_exprt(from_integer(0, type), result, complex_type);
   }
 
   return result;

src/util/c_types.cpp

@@ -182,23 +182,23 @@ unsignedbv_typet char32_t_type()
   return result;
 }
 
-bitvector_typet float_type()
+floatbv_typet float_type()
 {
   floatbv_typet result=
     ieee_float_spect::single_precision().to_type();
   result.set(ID_C_c_type, ID_float);
   return result;
 }
 
-bitvector_typet double_type()
+floatbv_typet double_type()
 {
   floatbv_typet result=
     ieee_float_spect::double_precision().to_type();
   result.set(ID_C_c_type, ID_double);
   return result;
 }
 
-bitvector_typet long_double_type()
+floatbv_typet long_double_type()
 {
   floatbv_typet result;
   if(config.ansi_c.long_double_width==128)

src/util/c_types.h

@@ -29,9 +29,9 @@ signedbv_typet signed_char_type();
 bitvector_typet wchar_t_type();
 unsignedbv_typet char16_t_type();
 unsignedbv_typet char32_t_type();
-bitvector_typet float_type();
-bitvector_typet double_type();
-bitvector_typet long_double_type();
+floatbv_typet float_type();
+floatbv_typet double_type();
+floatbv_typet long_double_type();
 unsignedbv_typet size_type();
 signedbv_typet signed_size_type();
 signedbv_typet pointer_diff_type();