Skip to content

bugfix: __float80 is a typedef, not a keyword #2629

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

bugfix: __float80 is a typedef, not a keyword #2629

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 11 additions & 1 deletion src/ansi-c/ansi_c_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,10 +195,20 @@ void ansi_c_internal_additions(std::string &code)
config.ansi_c.arch=="x86_64" ||
config.ansi_c.arch=="x32")
{
if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
code+="typedef double __float128;\n"; // clang doesn't do __float128
}

if(
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
{
// clang doesn't do __float80
// Note that __float80 is a typedef, and not a keyword.
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
code += "typedef __CPROVER_Float64x __float80;\n";
}

// On 64-bit systems, gcc has typedefs
// __int128_t und __uint128_t -- but not on 32 bit!
if(config.ansi_c.long_int_width>=64)
Expand Down
7 changes: 2 additions & 5 deletions src/ansi-c/scanner.l
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -489,11 +489,8 @@ void ansi_c_scanner_init()
return make_identifier();
}

"__float80" { // clang doesn't have it
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
{ loc(); return TOK_GCC_FLOAT80; }
else
return make_identifier();
"__CPROVER__Float64x" {
loc(); return TOK_GCC_FLOAT64X;
}

"__float128" { // clang doesn't have it
Expand Down
12 changes: 11 additions & 1 deletion src/cpp/cpp_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,10 +126,20 @@ void cpp_internal_additions(std::ostream &out)
config.ansi_c.arch == "x32")
{
// clang doesn't do __float128
if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE)
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
out << "typedef double __float128;" << '\n';
}

if(
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
{
// clang doesn't do __float80
// Note that __float80 is a typedef, and not a keyword.
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
out << "typedef __CPROVER_Float64x __float80;" << '\n';
}

// On 64-bit systems, gcc has typedefs
// __int128_t und __uint128_t -- but not on 32 bit!
if(config.ansi_c.long_int_width >= 64)
Expand Down