diff --git a/regression/cbmc/ts18661_typedefs/main.c b/regression/cbmc/ts18661_typedefs/main.c new file mode 100644 index 00000000000..06ef87fbc72 --- /dev/null +++ b/regression/cbmc/ts18661_typedefs/main.c @@ -0,0 +1,9 @@ +typedef float _Float32; +typedef double _Float32x; +typedef double _Float64; +typedef long double _Float64x; +typedef long double _Float128; +typedef long double _Float128x; + +int main(int argc, char** argv) { +} diff --git a/regression/cbmc/ts18661_typedefs/test.desc b/regression/cbmc/ts18661_typedefs/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/ts18661_typedefs/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 0ac703eebee..aa541a9d6e8 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -344,9 +344,22 @@ void ansi_c_convert_typet::write(typet &type) gcc_float64_cnt+gcc_float64x_cnt+ gcc_float128_cnt+gcc_float128x_cnt>=2) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; - throw 0; + // Temporary workaround for our glibc versions that try to define TS 18661 + // types (for example, typedef float _Float32). This can be removed once + // upgrade cbmc's GCC support to at least 7.0 (when glibc will expect us + // to provide these types natively), or disable parsing them ourselves + // when our preprocessor stage claims support <7.0. + if(c_storage_spec.is_typedef) + { + warning().source_location = source_location; + warning() << "ignoring typedef for TS 18661 (_FloatNNx) type. If you need these, try using goto-cc instead." << eom; + } + else + { + error().source_location=source_location; + error() << "conflicting type modifiers" << eom; + throw 0; + } } // _not_ the same as float, double, long double