Skip to content

Commit 928c28f

Browse files
author
Daniel Kroening
authored
Merge pull request #876 from tautschnig/gcc-builtins
Further extensions and automation to GCC built-in declarations
2 parents 0b62971 + 3f23794 commit 928c28f

17 files changed

+2568
-725
lines changed

‎.gitignore

+7
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,16 @@ src/ansi-c/gcc_builtin_headers_alpha.inc
2828
src/ansi-c/gcc_builtin_headers_arm.inc
2929
src/ansi-c/gcc_builtin_headers_generic.inc
3030
src/ansi-c/gcc_builtin_headers_ia32-2.inc
31+
src/ansi-c/gcc_builtin_headers_ia32-3.inc
32+
src/ansi-c/gcc_builtin_headers_ia32-4.inc
3133
src/ansi-c/gcc_builtin_headers_ia32.inc
34+
src/ansi-c/gcc_builtin_headers_math.inc
35+
src/ansi-c/gcc_builtin_headers_mem_string.inc
36+
src/ansi-c/gcc_builtin_headers_omp.inc
37+
src/ansi-c/gcc_builtin_headers_tm.inc
3238
src/ansi-c/gcc_builtin_headers_mips.inc
3339
src/ansi-c/gcc_builtin_headers_power.inc
40+
src/ansi-c/gcc_builtin_headers_ubsan.inc
3441

3542
# regression/test files
3643
*.out

‎scripts/cpplint.py

+4-1
Original file line numberDiff line numberDiff line change
@@ -6471,7 +6471,10 @@ def ProcessFile(filename, vlevel, extra_check_functions=[]):
64716471
_BackupFilters()
64726472

64736473
#exclude these files:
6474-
if Search(r'(\.l|\.y|\.inc|\.d|\.o|y\.tab\.cpp|\.tab\.h|\.yy\.cpp|builtin_headers)$', filename):
6474+
if Search(r'(\.l|\.y|\.inc|\.d|\.o|y\.tab\.cpp|\.tab\.h|\.yy\.cpp)$', filename):
6475+
return
6476+
6477+
if Search(r'_builtin_headers_[a-z0-9_-]+\.h$', filename):
64756478
return
64766479

64776480
if not ProcessConfigOverrides(filename):

‎src/ansi-c/Makefile

+17-2
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,11 @@ CLEANFILES = ansi-c$(LIBEXT) \
5454
arm_builtin_headers.inc cw_builtin_headers.inc \
5555
gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \
5656
gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \
57-
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc
57+
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
58+
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
59+
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
60+
gcc_builtin_headers_mem_string.inc \
61+
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
5862

5963
all: ansi-c$(LIBEXT)
6064

@@ -115,10 +119,17 @@ cprover_library.cpp: cprover_library.inc
115119
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
116120
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
117121
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
122+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
123+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
118124
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
119125
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
126+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
127+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc
120128
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc
129+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc
121130
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc
131+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc
132+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc
122133
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
123134
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
124135
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc
@@ -128,7 +139,11 @@ generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
128139
gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \
129140
gcc_builtin_headers_power.inc arm_builtin_headers.inc \
130141
cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \
131-
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc
142+
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
143+
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
144+
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
145+
gcc_builtin_headers_mem_string.inc \
146+
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
132147

133148
###############################################################################
134149

‎src/ansi-c/ansi_c_internal_additions.cpp

+38
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,44 @@ const char gcc_builtin_headers_generic[]=
1515
#include "gcc_builtin_headers_generic.inc"
1616
; // NOLINT(whitespace/semicolon)
1717

18+
const char gcc_builtin_headers_math[]=
19+
"# 1 \"gcc_builtin_headers_math.h\"\n"
20+
#include "gcc_builtin_headers_math.inc"
21+
; // NOLINT(whitespace/semicolon)
22+
23+
const char gcc_builtin_headers_mem_string[]=
24+
"# 1 \"gcc_builtin_headers_mem_string.h\"\n"
25+
#include "gcc_builtin_headers_mem_string.inc"
26+
; // NOLINT(whitespace/semicolon)
27+
28+
const char gcc_builtin_headers_omp[]=
29+
"# 1 \"gcc_builtin_headers_omp.h\"\n"
30+
#include "gcc_builtin_headers_omp.inc"
31+
; // NOLINT(whitespace/semicolon)
32+
33+
const char gcc_builtin_headers_tm[]=
34+
"# 1 \"gcc_builtin_headers_tm.h\"\n"
35+
#include "gcc_builtin_headers_tm.inc"
36+
; // NOLINT(whitespace/semicolon)
37+
38+
const char gcc_builtin_headers_ubsan[]=
39+
"# 1 \"gcc_builtin_headers_ubsan.h\"\n"
40+
#include "gcc_builtin_headers_ubsan.inc"
41+
; // NOLINT(whitespace/semicolon)
42+
1843
const char gcc_builtin_headers_ia32[]=
1944
"# 1 \"gcc_builtin_headers_ia32.h\"\n"
2045
#include "gcc_builtin_headers_ia32.inc"
2146
; // NOLINT(whitespace/semicolon)
2247
const char gcc_builtin_headers_ia32_2[]=
2348
#include "gcc_builtin_headers_ia32-2.inc"
2449
; // NOLINT(whitespace/semicolon)
50+
const char gcc_builtin_headers_ia32_3[]=
51+
#include "gcc_builtin_headers_ia32-3.inc"
52+
; // NOLINT(whitespace/semicolon)
53+
const char gcc_builtin_headers_ia32_4[]=
54+
#include "gcc_builtin_headers_ia32-4.inc"
55+
; // NOLINT(whitespace/semicolon)
2556

2657
const char gcc_builtin_headers_alpha[]=
2758
"# 1 \"gcc_builtin_headers_alpha.h\"\n"
@@ -244,6 +275,11 @@ void ansi_c_internal_additions(std::string &code)
244275
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
245276
{
246277
code+=gcc_builtin_headers_generic;
278+
code+=gcc_builtin_headers_math;
279+
code+=gcc_builtin_headers_mem_string;
280+
code+=gcc_builtin_headers_omp;
281+
code+=gcc_builtin_headers_tm;
282+
code+=gcc_builtin_headers_ubsan;
247283
code+=clang_builtin_headers;
248284

249285
// there are many more, e.g., look at
@@ -258,6 +294,8 @@ void ansi_c_internal_additions(std::string &code)
258294

259295
code+=gcc_builtin_headers_ia32;
260296
code+=gcc_builtin_headers_ia32_2;
297+
code+=gcc_builtin_headers_ia32_3;
298+
code+=gcc_builtin_headers_ia32_4;
261299
}
262300
else if(config.ansi_c.arch=="arm64" ||
263301
config.ansi_c.arch=="armel" ||

‎src/ansi-c/ansi_c_internal_additions.h

+9
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,16 @@ void ansi_c_internal_additions(std::string &code);
1515
void ansi_c_architecture_strings(std::string &code);
1616

1717
extern const char gcc_builtin_headers_generic[];
18+
extern const char gcc_builtin_headers_math[];
19+
extern const char gcc_builtin_headers_mem_string[];
20+
extern const char gcc_builtin_headers_omp[];
21+
extern const char gcc_builtin_headers_tm[];
22+
extern const char gcc_builtin_headers_ubsan[];
23+
extern const char clang_builtin_headers[];
1824
extern const char gcc_builtin_headers_ia32[];
25+
extern const char gcc_builtin_headers_ia32_2[];
26+
extern const char gcc_builtin_headers_ia32_3[];
27+
extern const char gcc_builtin_headers_ia32_4[];
1928
extern const char arm_builtin_headers[];
2029

2130
#endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H

0 commit comments

Comments
 (0)