diff --git a/src/ansi-c/gcc_types.cpp b/src/ansi-c/gcc_types.cpp index cebc072e5fc..f16e9bc8784 100644 --- a/src/ansi-c/gcc_types.cpp +++ b/src/ansi-c/gcc_types.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -bitvector_typet gcc_float16_type() +floatbv_typet gcc_float16_type() { floatbv_typet result= ieee_float_spect::half_precision().to_type(); @@ -19,7 +19,7 @@ bitvector_typet gcc_float16_type() 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= diff --git a/src/ansi-c/gcc_types.h b/src/ansi-c/gcc_types.h index 95f4b4957d7..5da8d291cce 100644 --- a/src/ansi-c/gcc_types.h +++ b/src/ansi-c/gcc_types.h @@ -14,13 +14,13 @@ Author: Daniel Kroening, kroening@kroening.com // 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(); diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index 35599d1bf7d..cfbb9c0bf8f 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -25,48 +25,49 @@ Author: Daniel Kroening, kroening@kroening.com #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; diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp index c0cd6cc37a8..33db616c46b 100644 --- a/src/util/c_types.cpp +++ b/src/util/c_types.cpp @@ -182,7 +182,7 @@ 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(); @@ -190,7 +190,7 @@ bitvector_typet float_type() return result; } -bitvector_typet double_type() +floatbv_typet double_type() { floatbv_typet result= ieee_float_spect::double_precision().to_type(); @@ -198,7 +198,7 @@ bitvector_typet double_type() return result; } -bitvector_typet long_double_type() +floatbv_typet long_double_type() { floatbv_typet result; if(config.ansi_c.long_double_width==128) diff --git a/src/util/c_types.h b/src/util/c_types.h index b80851ce97a..9e97d19f266 100644 --- a/src/util/c_types.h +++ b/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();