gcc floating-point types now return a float_typet

Author: Daniel 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();