Merge pull request #3114 from diffblue/c_float_types

float_type(), double_type() and long_double_type() now return float_typet

Author: kroening

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/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();