Skip to content

Further extensions and automation to GCC built-in declarations #876

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 7 commits into from
May 29, 2017
Merged

Further extensions and automation to GCC built-in declarations #876

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
f0fe020
Make the linter ignore generated builtin-header files
tautschnig May 23, 2017
01b8240
get-gcc-builtins: only dump declarations not found in existing files
tautschnig Apr 26, 2017
98e5c23
Split generic GCC built-ins, extend using current GCC trunk
tautschnig Apr 26, 2017
b4eaa3d
get-gcc-builtins.sh: extract ia32 declarations automatically
tautschnig Apr 27, 2017
bf3a45a
builtin-headers-ia32: remove space before '*'
tautschnig Apr 27, 2017
0bdac88
Updates to ia32 headers by get-gcc-builtins.sh
tautschnig Apr 27, 2017
3f23794
Added further ia32 GCC built-ins
tautschnig Apr 27, 2017
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
7 changes: 7 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,16 @@ src/ansi-c/gcc_builtin_headers_alpha.inc
src/ansi-c/gcc_builtin_headers_arm.inc
src/ansi-c/gcc_builtin_headers_generic.inc
src/ansi-c/gcc_builtin_headers_ia32-2.inc
src/ansi-c/gcc_builtin_headers_ia32-3.inc
src/ansi-c/gcc_builtin_headers_ia32-4.inc
src/ansi-c/gcc_builtin_headers_ia32.inc
src/ansi-c/gcc_builtin_headers_math.inc
src/ansi-c/gcc_builtin_headers_mem_string.inc
src/ansi-c/gcc_builtin_headers_omp.inc
src/ansi-c/gcc_builtin_headers_tm.inc
src/ansi-c/gcc_builtin_headers_mips.inc
src/ansi-c/gcc_builtin_headers_power.inc
src/ansi-c/gcc_builtin_headers_ubsan.inc

# regression/test files
*.out
Expand Down
5 changes: 4 additions & 1 deletion scripts/cpplint.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6471,7 +6471,10 @@ def ProcessFile(filename, vlevel, extra_check_functions=[]):
_BackupFilters()

#exclude these files:
if Search(r'(\.l|\.y|\.inc|\.d|\.o|y\.tab\.cpp|\.tab\.h|\.yy\.cpp|builtin_headers)$', filename):
if Search(r'(\.l|\.y|\.inc|\.d|\.o|y\.tab\.cpp|\.tab\.h|\.yy\.cpp)$', filename):
return

if Search(r'_builtin_headers_[a-z0-9_-]+\.h$', filename):
return

if not ProcessConfigOverrides(filename):
Expand Down
19 changes: 17 additions & 2 deletions src/ansi-c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,11 @@ CLEANFILES = ansi-c$(LIBEXT) \
arm_builtin_headers.inc cw_builtin_headers.inc \
gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \
gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
gcc_builtin_headers_mem_string.inc \
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc

all: ansi-c$(LIBEXT)

Expand Down Expand Up @@ -116,10 +120,17 @@ cprover_library.cpp: cprover_library.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc
Expand All @@ -129,7 +140,11 @@ generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \
gcc_builtin_headers_power.inc arm_builtin_headers.inc \
cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
gcc_builtin_headers_mem_string.inc \
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc

###############################################################################

Expand Down
38 changes: 38 additions & 0 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 @@ -15,13 +15,44 @@ const char gcc_builtin_headers_generic[]=
#include "gcc_builtin_headers_generic.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_math[]=
"# 1 \"gcc_builtin_headers_math.h\"\n"
#include "gcc_builtin_headers_math.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_mem_string[]=
"# 1 \"gcc_builtin_headers_mem_string.h\"\n"
#include "gcc_builtin_headers_mem_string.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_omp[]=
"# 1 \"gcc_builtin_headers_omp.h\"\n"
#include "gcc_builtin_headers_omp.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_tm[]=
"# 1 \"gcc_builtin_headers_tm.h\"\n"
#include "gcc_builtin_headers_tm.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_ubsan[]=
"# 1 \"gcc_builtin_headers_ubsan.h\"\n"
#include "gcc_builtin_headers_ubsan.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_ia32[]=
"# 1 \"gcc_builtin_headers_ia32.h\"\n"
#include "gcc_builtin_headers_ia32.inc"
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_2[]=
#include "gcc_builtin_headers_ia32-2.inc"
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_3[]=
#include "gcc_builtin_headers_ia32-3.inc"
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_4[]=
#include "gcc_builtin_headers_ia32-4.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_alpha[]=
"# 1 \"gcc_builtin_headers_alpha.h\"\n"
Expand Down Expand Up @@ -242,6 +273,11 @@ void ansi_c_internal_additions(std::string &code)
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
{
code+=gcc_builtin_headers_generic;
code+=gcc_builtin_headers_math;
code+=gcc_builtin_headers_mem_string;
code+=gcc_builtin_headers_omp;
code+=gcc_builtin_headers_tm;
code+=gcc_builtin_headers_ubsan;
code+=clang_builtin_headers;

// there are many more, e.g., look at
Expand All @@ -256,6 +292,8 @@ void ansi_c_internal_additions(std::string &code)

code+=gcc_builtin_headers_ia32;
code+=gcc_builtin_headers_ia32_2;
code+=gcc_builtin_headers_ia32_3;
code+=gcc_builtin_headers_ia32_4;
}
else if(config.ansi_c.arch=="arm64" ||
config.ansi_c.arch=="armel" ||
Expand Down
9 changes: 9 additions & 0 deletions src/ansi-c/ansi_c_internal_additions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,16 @@ void ansi_c_internal_additions(std::string &code);
void ansi_c_architecture_strings(std::string &code);

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 clang_builtin_headers[];
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 arm_builtin_headers[];

#endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H
Loading