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

Author: kroening

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