on-demand definitions for compiler-built-in functions #1910
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -10,6 +10,11 @@ Author: Daniel Kroening, [email protected] | |
|
|
||
| #include <util/config.h> | ||
|
|
||
| const char gcc_builtin_headers_types[]= | ||
| "# 1 \"gcc_builtin_headers_types.h\"\n" | ||
| #include "gcc_builtin_headers_types.inc" | ||
| ; // NOLINT(whitespace/semicolon) | ||
|
|
||
| const char gcc_builtin_headers_generic[]= | ||
| "# 1 \"gcc_builtin_headers_generic.h\"\n" | ||
| #include "gcc_builtin_headers_generic.inc" | ||
|
|
@@ -89,6 +94,10 @@ const char clang_builtin_headers[]= | |
| #include "clang_builtin_headers.inc" | ||
| ; // NOLINT(whitespace/semicolon) | ||
|
|
||
| const char windows_builtin_headers[]= | ||
| "int __noop();\n" | ||
|
There was a problem hiding this comment. Should this have a file name as the others do? There was a problem hiding this comment. Seemed unnecessary luxury for two lines. There was a problem hiding this comment. One day those 2 lines will be 10 and no-one will notice that they should have inserted the file name. It's near zero cost right now, but it might prove costly later. |
||
| "int __assume(int);\n"; | ||
|
|
||
| static std::string architecture_string(const std::string &value, const char *s) | ||
| { | ||
| return std::string("const char *__CPROVER_architecture_")+ | ||
|
|
@@ -257,13 +266,7 @@ void ansi_c_internal_additions(std::string &code) | |
| config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || | ||
| 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 | ||
|
|
@@ -274,37 +277,6 @@ void ansi_c_internal_additions(std::string &code) | |
| { | ||
| if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE) | ||
| code+="typedef double __float128;\n"; // clang doesn't do __float128 | ||
| } | ||
|
|
||
| // On 64-bit systems, gcc has typedefs | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -15,17 +15,24 @@ Author: Daniel Kroening, [email protected] | |
| void ansi_c_internal_additions(std::string &code); | ||
| void ansi_c_architecture_strings(std::string &code); | ||
|
|
||
| extern const char clang_builtin_headers[]; | ||
| extern const char gcc_builtin_headers_types[]; | ||
| extern const char gcc_builtin_headers_generic[]; | ||
| extern const char gcc_builtin_headers_math[]; | ||
| extern const char gcc_builtin_headers_mem_string[]; | ||
| extern const char gcc_builtin_headers_omp[]; | ||
| extern const char gcc_builtin_headers_tm[]; | ||
| extern const char gcc_builtin_headers_ubsan[]; | ||
| extern const char gcc_builtin_headers_ia32[]; | ||
| extern const char gcc_builtin_headers_ia32_2[]; | ||
| extern const char gcc_builtin_headers_ia32_3[]; | ||
| extern const char gcc_builtin_headers_ia32_4[]; | ||
| extern const char gcc_builtin_headers_alpha[]; | ||
| extern const char gcc_builtin_headers_arm[]; | ||
| extern const char gcc_builtin_headers_mips[]; | ||
| extern const char gcc_builtin_headers_power[]; | ||
| extern const char arm_builtin_headers[]; | ||
| extern const char cw_builtin_headers[]; | ||
| extern const char windows_builtin_headers[]; | ||
|
|
||
| #endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
While at this, would it be possible to introduce a Makefile variable holding all the header files? As is, the same list of files appears three times.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done