Skip to content

Commit 6022a46

Browse files
tautschnigtautschnig
committed
Move declarations of non-cprover intrinsics to subdirectory
This is to make them easier to distinguish from any other header files: the declarations located in these files may need to be updated from time to time. The frequency of those updates, however, depends on the release cadence by other compilers. It is unrelated to our release cadence.
1 parent d932d6f commit 6022a46

25 files changed

+104
-100
lines changed

‎src/ansi-c/CMakeLists.txt

Lines changed: 42 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,9 @@ add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
1212
add_executable(file_converter file_converter.cpp)
1313

1414
function(make_inc name)
15+
get_filename_component(inc_path "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc" DIRECTORY)
1516
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc"
17+
COMMAND ${CMAKE_COMMAND} -E make_directory ${inc_path}
1618
COMMAND file_converter "${CMAKE_CURRENT_SOURCE_DIR}/${name}.h" > "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc"
1719
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${name}.h" file_converter
1820
)
@@ -52,51 +54,51 @@ endif()
5254

5355
################################################################################
5456

55-
make_inc(arm_builtin_headers)
56-
make_inc(clang_builtin_headers)
57+
make_inc(compiler_headers/arm_builtin_headers)
58+
make_inc(compiler_headers/clang_builtin_headers)
59+
make_inc(compiler_headers/cw_builtin_headers)
60+
make_inc(compiler_headers/gcc_builtin_headers_alpha)
61+
make_inc(compiler_headers/gcc_builtin_headers_arm)
62+
make_inc(compiler_headers/gcc_builtin_headers_generic)
63+
make_inc(compiler_headers/gcc_builtin_headers_ia32)
64+
make_inc(compiler_headers/gcc_builtin_headers_ia32-2)
65+
make_inc(compiler_headers/gcc_builtin_headers_ia32-3)
66+
make_inc(compiler_headers/gcc_builtin_headers_ia32-4)
67+
make_inc(compiler_headers/gcc_builtin_headers_ia32-5)
68+
make_inc(compiler_headers/gcc_builtin_headers_math)
69+
make_inc(compiler_headers/gcc_builtin_headers_mem_string)
70+
make_inc(compiler_headers/gcc_builtin_headers_mips)
71+
make_inc(compiler_headers/gcc_builtin_headers_omp)
72+
make_inc(compiler_headers/gcc_builtin_headers_power)
73+
make_inc(compiler_headers/gcc_builtin_headers_tm)
74+
make_inc(compiler_headers/gcc_builtin_headers_types)
75+
make_inc(compiler_headers/gcc_builtin_headers_ubsan)
76+
make_inc(compiler_headers/windows_builtin_headers)
5777
make_inc(cprover_builtin_headers)
58-
make_inc(cw_builtin_headers)
59-
make_inc(gcc_builtin_headers_alpha)
60-
make_inc(gcc_builtin_headers_arm)
61-
make_inc(gcc_builtin_headers_generic)
62-
make_inc(gcc_builtin_headers_ia32)
63-
make_inc(gcc_builtin_headers_ia32-2)
64-
make_inc(gcc_builtin_headers_ia32-3)
65-
make_inc(gcc_builtin_headers_ia32-4)
66-
make_inc(gcc_builtin_headers_ia32-5)
67-
make_inc(gcc_builtin_headers_math)
68-
make_inc(gcc_builtin_headers_mem_string)
69-
make_inc(gcc_builtin_headers_mips)
70-
make_inc(gcc_builtin_headers_omp)
71-
make_inc(gcc_builtin_headers_power)
72-
make_inc(gcc_builtin_headers_tm)
73-
make_inc(gcc_builtin_headers_types)
74-
make_inc(gcc_builtin_headers_ubsan)
75-
make_inc(windows_builtin_headers)
7678

7779
set(extra_dependencies
78-
${CMAKE_CURRENT_BINARY_DIR}/arm_builtin_headers.inc
79-
${CMAKE_CURRENT_BINARY_DIR}/clang_builtin_headers.inc
80+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/arm_builtin_headers.inc
81+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/clang_builtin_headers.inc
82+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/cw_builtin_headers.inc
83+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_alpha.inc
84+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_arm.inc
85+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_generic.inc
86+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-2.inc
87+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-3.inc
88+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-4.inc
89+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-5.inc
90+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32.inc
91+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_math.inc
92+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mem_string.inc
93+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mips.inc
94+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_omp.inc
95+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_power.inc
96+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_tm.inc
97+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types.inc
98+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ubsan.inc
99+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/windows_builtin_headers.inc
80100
${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
81101
${CMAKE_CURRENT_BINARY_DIR}/cprover_builtin_headers.inc
82-
${CMAKE_CURRENT_BINARY_DIR}/cw_builtin_headers.inc
83-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_alpha.inc
84-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_arm.inc
85-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_generic.inc
86-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
87-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
88-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
89-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-5.inc
90-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
91-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
92-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc
93-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mips.inc
94-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc
95-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc
96-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc
97-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_types.inc
98-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
99-
${CMAKE_CURRENT_BINARY_DIR}/windows_builtin_headers.inc
100102
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
101103
)
102104

‎src/ansi-c/Makefile

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -49,27 +49,27 @@ include ../config.inc
4949
include ../common
5050

5151
BUILTIN_FILES = \
52-
arm_builtin_headers.inc \
53-
clang_builtin_headers.inc \
5452
cprover_builtin_headers.inc \
55-
cw_builtin_headers.inc \
56-
gcc_builtin_headers_alpha.inc \
57-
gcc_builtin_headers_arm.inc \
58-
gcc_builtin_headers_generic.inc \
59-
gcc_builtin_headers_ia32-2.inc \
60-
gcc_builtin_headers_ia32-3.inc \
61-
gcc_builtin_headers_ia32-4.inc \
62-
gcc_builtin_headers_ia32-5.inc \
63-
gcc_builtin_headers_ia32.inc \
64-
gcc_builtin_headers_math.inc \
65-
gcc_builtin_headers_mem_string.inc \
66-
gcc_builtin_headers_mips.inc \
67-
gcc_builtin_headers_omp.inc \
68-
gcc_builtin_headers_power.inc \
69-
gcc_builtin_headers_tm.inc \
70-
gcc_builtin_headers_types.inc \
71-
gcc_builtin_headers_ubsan.inc \
72-
windows_builtin_headers.inc
53+
compiler_headers/arm_builtin_headers.inc \
54+
compiler_headers/clang_builtin_headers.inc \
55+
compiler_headers/cw_builtin_headers.inc \
56+
compiler_headers/gcc_builtin_headers_alpha.inc \
57+
compiler_headers/gcc_builtin_headers_arm.inc \
58+
compiler_headers/gcc_builtin_headers_generic.inc \
59+
compiler_headers/gcc_builtin_headers_ia32-2.inc \
60+
compiler_headers/gcc_builtin_headers_ia32-3.inc \
61+
compiler_headers/gcc_builtin_headers_ia32-4.inc \
62+
compiler_headers/gcc_builtin_headers_ia32-5.inc \
63+
compiler_headers/gcc_builtin_headers_ia32.inc \
64+
compiler_headers/gcc_builtin_headers_math.inc \
65+
compiler_headers/gcc_builtin_headers_mem_string.inc \
66+
compiler_headers/gcc_builtin_headers_mips.inc \
67+
compiler_headers/gcc_builtin_headers_omp.inc \
68+
compiler_headers/gcc_builtin_headers_power.inc \
69+
compiler_headers/gcc_builtin_headers_tm.inc \
70+
compiler_headers/gcc_builtin_headers_types.inc \
71+
compiler_headers/gcc_builtin_headers_ubsan.inc \
72+
compiler_headers/windows_builtin_headers.inc
7373

7474
CLEANFILES = ansi-c$(LIBEXT) \
7575
ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 41 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -17,92 +17,93 @@ Author: Daniel Kroening, [email protected]
1717

1818
const char gcc_builtin_headers_types[] =
1919
"#line 1 \"gcc_builtin_headers_types.h\"\n"
20-
#include "gcc_builtin_headers_types.inc" // IWYU pragma: keep
21-
; // NOLINT(whitespace/semicolon)
20+
#include "compiler_headers/gcc_builtin_headers_types.inc" // IWYU pragma: keep
21+
; // NOLINT(whitespace/semicolon)
2222

2323
const char gcc_builtin_headers_generic[] =
2424
"#line 1 \"gcc_builtin_headers_generic.h\"\n"
25-
#include "gcc_builtin_headers_generic.inc" // IWYU pragma: keep
26-
; // NOLINT(whitespace/semicolon)
25+
#include "compiler_headers/gcc_builtin_headers_generic.inc" // IWYU pragma: keep
26+
; // NOLINT(whitespace/semicolon)
2727

2828
const char gcc_builtin_headers_math[] =
2929
"#line 1 \"gcc_builtin_headers_math.h\"\n"
30-
#include "gcc_builtin_headers_math.inc" // IWYU pragma: keep
31-
; // NOLINT(whitespace/semicolon)
30+
#include "compiler_headers/gcc_builtin_headers_math.inc" // IWYU pragma: keep
31+
; // NOLINT(whitespace/semicolon)
3232

3333
const char gcc_builtin_headers_mem_string[] =
3434
"#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
35-
#include "gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
36-
; // NOLINT(whitespace/semicolon)
35+
// NOLINTNEXTLINE(whitespace/line_length)
36+
#include "compiler_headers/gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
37+
; // NOLINT(whitespace/semicolon)
3738

3839
const char gcc_builtin_headers_omp[] = "#line 1 \"gcc_builtin_headers_omp.h\"\n"
39-
#include "gcc_builtin_headers_omp.inc" // IWYU pragma: keep
40-
; // NOLINT(whitespace/semicolon)
40+
#include "compiler_headers/gcc_builtin_headers_omp.inc" // IWYU pragma: keep
41+
; // NOLINT(whitespace/semicolon)
4142

4243
const char gcc_builtin_headers_tm[] = "#line 1 \"gcc_builtin_headers_tm.h\"\n"
43-
#include "gcc_builtin_headers_tm.inc" // IWYU pragma: keep
44-
; // NOLINT(whitespace/semicolon)
44+
#include "compiler_headers/gcc_builtin_headers_tm.inc" // IWYU pragma: keep
45+
; // NOLINT(whitespace/semicolon)
4546

4647
const char gcc_builtin_headers_ubsan[] =
4748
"#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
48-
#include "gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
49-
; // NOLINT(whitespace/semicolon)
49+
#include "compiler_headers/gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
50+
; // NOLINT(whitespace/semicolon)
5051

5152
const char gcc_builtin_headers_ia32[] =
5253
"#line 1 \"gcc_builtin_headers_ia32.h\"\n"
53-
#include "gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
54-
; // NOLINT(whitespace/semicolon)
54+
#include "compiler_headers/gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
55+
; // NOLINT(whitespace/semicolon)
5556
const char gcc_builtin_headers_ia32_2[] =
56-
#include "gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
57-
; // NOLINT(whitespace/semicolon)
57+
#include "compiler_headers/gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
58+
; // NOLINT(whitespace/semicolon)
5859
const char gcc_builtin_headers_ia32_3[] =
59-
#include "gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
60-
; // NOLINT(whitespace/semicolon)
60+
#include "compiler_headers/gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
61+
; // NOLINT(whitespace/semicolon)
6162
const char gcc_builtin_headers_ia32_4[] =
62-
#include "gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
63-
; // NOLINT(whitespace/semicolon)
63+
#include "compiler_headers/gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
64+
; // NOLINT(whitespace/semicolon)
6465
const char gcc_builtin_headers_ia32_5[] =
65-
#include "gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
66-
; // NOLINT(whitespace/semicolon)
66+
#include "compiler_headers/gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
67+
; // NOLINT(whitespace/semicolon)
6768

6869
const char gcc_builtin_headers_alpha[] =
6970
"#line 1 \"gcc_builtin_headers_alpha.h\"\n"
70-
#include "gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
71-
; // NOLINT(whitespace/semicolon)
71+
#include "compiler_headers/gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
72+
; // NOLINT(whitespace/semicolon)
7273

7374
const char gcc_builtin_headers_arm[] = "#line 1 \"gcc_builtin_headers_arm.h\"\n"
74-
#include "gcc_builtin_headers_arm.inc" // IWYU pragma: keep
75-
; // NOLINT(whitespace/semicolon)
75+
#include "compiler_headers/gcc_builtin_headers_arm.inc" // IWYU pragma: keep
76+
; // NOLINT(whitespace/semicolon)
7677

7778
const char gcc_builtin_headers_mips[] =
7879
"#line 1 \"gcc_builtin_headers_mips.h\"\n"
79-
#include "gcc_builtin_headers_mips.inc" // IWYU pragma: keep
80-
; // NOLINT(whitespace/semicolon)
80+
#include "compiler_headers/gcc_builtin_headers_mips.inc" // IWYU pragma: keep
81+
; // NOLINT(whitespace/semicolon)
8182

8283
const char gcc_builtin_headers_power[] =
8384
"#line 1 \"gcc_builtin_headers_power.h\"\n"
84-
#include "gcc_builtin_headers_power.inc" // IWYU pragma: keep
85-
; // NOLINT(whitespace/semicolon)
85+
#include "compiler_headers/gcc_builtin_headers_power.inc" // IWYU pragma: keep
86+
; // NOLINT(whitespace/semicolon)
8687

8788
const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n"
88-
#include "arm_builtin_headers.inc" // IWYU pragma: keep
89-
; // NOLINT(whitespace/semicolon)
89+
#include "compiler_headers/arm_builtin_headers.inc" // IWYU pragma: keep
90+
; // NOLINT(whitespace/semicolon)
9091

9192
const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n"
92-
#include "cw_builtin_headers.inc" // IWYU pragma: keep
93-
; // NOLINT(whitespace/semicolon)
93+
#include "compiler_headers/cw_builtin_headers.inc" // IWYU pragma: keep
94+
; // NOLINT(whitespace/semicolon)
9495

9596
const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n"
96-
#include "clang_builtin_headers.inc" // IWYU pragma: keep
97-
; // NOLINT(whitespace/semicolon)
97+
#include "compiler_headers/clang_builtin_headers.inc" // IWYU pragma: keep
98+
; // NOLINT(whitespace/semicolon)
9899

99100
const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n"
100101
#include "cprover_builtin_headers.inc" // IWYU pragma: keep
101102
; // NOLINT(whitespace/semicolon)
102103

103104
const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n"
104-
#include "windows_builtin_headers.inc" // IWYU pragma: keep
105-
; // NOLINT(whitespace/semicolon)
105+
#include "compiler_headers/windows_builtin_headers.inc" // IWYU pragma: keep
106+
; // NOLINT(whitespace/semicolon)
106107

107108
static std::string architecture_string(const std::string &value, const char *s)
108109
{

‎src/ansi-c/arm_builtin_headers.h renamed to ‎src/ansi-c/compiler_headers/arm_builtin_headers.h

File renamed without changes.

‎src/ansi-c/clang_builtin_headers.h renamed to ‎src/ansi-c/compiler_headers/clang_builtin_headers.h

File renamed without changes.

‎src/ansi-c/cw_builtin_headers.h renamed to ‎src/ansi-c/compiler_headers/cw_builtin_headers.h

File renamed without changes.

‎src/ansi-c/gcc_builtin_headers_alpha.h renamed to ‎src/ansi-c/compiler_headers/gcc_builtin_headers_alpha.h

File renamed without changes.

‎src/ansi-c/gcc_builtin_headers_arm.h renamed to ‎src/ansi-c/compiler_headers/gcc_builtin_headers_arm.h

File renamed without changes.

‎src/ansi-c/gcc_builtin_headers_generic.h renamed to ‎src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h

File renamed without changes.

‎src/ansi-c/gcc_builtin_headers_ia32-2.h renamed to ‎src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-2.h

File renamed without changes.

0 commit comments

Comments
 (0)