Skip to content

ansi-c: clang extensions #2628

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

Merged
merged 6 commits into from
Jul 30, 2018
Merged

ansi-c: clang extensions #2628

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3849bb0
rename APPLE flavor to CLANG
Jul 28, 2018
16a49a7
bugfix: __float128
Jul 28, 2018
e63402e
added _Null_unspecified clang extension
Jul 28, 2018
5495625
FreeBSD: default flavor is now CLANG
Jul 28, 2018
8288a72
__float80 is a typedef, not a keyword
Jul 28, 2018
f74c161
test for __float80 and __float128
Jul 30, 2018
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
19 changes: 19 additions & 0 deletions regression/ansi-c/gcc_float_types1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// for gcc, __float80 and __float128 are typedefs
// for clang, __float128 is a keyword, and __float80 doesn't exist.

#ifdef __clang__
int __float80;
__float128 f128;
#else
__float80 f80;
__float128 f128;
#endif

int main()
{
#ifndef __clang__
// on gcc, they can be re-declared, as they are identifiers, not keywords
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps run the test against Clang too, but checking for the expected syntax error in the .desc file?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't have means to enable clang as preprocessor.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

goto-cc --native-compiler=clang should do so, I believe?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes; are we willing to add clang as a dependency for CI for this?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd say it's more an "in principle we could" case. We'll probably do if/when we run into a regression on this :-)

int __float80;
int __float128;
#endif
}
8 changes: 8 additions & 0 deletions regression/ansi-c/gcc_float_types1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
7 changes: 4 additions & 3 deletions src/ansi-c/ansi_c_declaration.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,9 +150,10 @@ void ansi_c_declarationt::to_symbol(
if(get_is_inline())
symbol.type.set(ID_C_inlined, true);

if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
if(
config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
{
// GCC extern inline cleanup, to enable remove_internal_symbols
// do its full job
Expand Down
40 changes: 32 additions & 8 deletions 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 @@ -182,21 +182,45 @@ void ansi_c_internal_additions(std::string &code)
"\n";

// GCC junk stuff, also for CLANG and ARM
if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
if(
config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
{
code+=gcc_builtin_headers_types;

// there are many more, e.g., look at
// https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html

if(config.ansi_c.arch=="i386" ||
config.ansi_c.arch=="x86_64" ||
config.ansi_c.arch=="x32")
if(
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
config.ansi_c.arch == "ia64")
{
if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
code+="typedef double __float128;\n"; // clang doesn't do __float128
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
// For clang, __float128 is a keyword.
// For gcc, this is a typedef and not a keyword.
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
code += "typedef __CPROVER_Float128 __float128;\n";
}
else if(config.ansi_c.arch == "hppa")
{
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
// For clang, __float128 is a keyword.
// For gcc, this is a typedef and not a keyword.
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
code+="typedef long 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)
code += "typedef __CPROVER_Float64x __float80;\n";
}

// On 64-bit systems, gcc has typedefs
Expand Down
7 changes: 4 additions & 3 deletions src/ansi-c/builtin_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,9 +134,10 @@ bool builtin_factory(
}

// GCC junk stuff, also for CLANG and ARM
if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
if(
config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
{
if(find_pattern(pattern, gcc_builtin_headers_generic, s))
return convert(identifier, s, symbol_table, mh);
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_base.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -336,7 +336,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
if(
old_symbol.type.get_bool(ID_C_inlined) &&
(config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE ||
config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
config.ansi_c.mode == configt::ansi_ct::flavourt::ARM ||
config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO))
{
Expand Down
8 changes: 4 additions & 4 deletions src/ansi-c/gcc_builtin_headers_ia32.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
// from
// http://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/X86-Built_002din-Functions.html

__float128 __builtin_fabsq(__float128);
__float128 __builtin_copysignq(__float128, __float128);
__CPROVER_Float128 __builtin_fabsq(__CPROVER_Float128);
__CPROVER_Float128 __builtin_copysignq(__CPROVER_Float128, __CPROVER_Float128);
void __builtin_ia32_pause();
__float128 __builtin_infq(void);
__float128 __builtin_huge_valq(void);
__CPROVER_Float128 __builtin_infq(void);
__CPROVER_Float128 __builtin_huge_valq(void);
__gcc_v8qi __builtin_ia32_paddb(__gcc_v8qi, __gcc_v8qi);
__gcc_v4hi __builtin_ia32_paddw(__gcc_v4hi, __gcc_v4hi);
__gcc_v2si __builtin_ia32_paddd(__gcc_v2si, __gcc_v2si);
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/get-gcc-builtins.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ cat > builtins.h <<EOF
// some newer versions of GCC apparently support __floatXYZ
#define dfloat32_type_node __float32
#define dfloat64_type_node __float64
#define dfloat128_type_node __float128
#define dfloat128_type_node __CPROVER_Float128
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Randomly placing this comment: the commit message says "bugfix" but it's not clear how this bug has been found/how a future regression is avoided?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was found by running the existing regressions on FreeBSD, and repeating that should avoid it in the future as well.


#define build_qualified_type(t, q) q t
#define build_pointer_type(t) t*
Expand Down
Loading