From 73551e058a850297bc72924a69b39affcfa49dfa Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 17:22:33 +0100 Subject: C parser: handle other built-in types than __builtin_va_list All the built-in types declared in $ARCH/CBuiltins.ml are now recognized as type names initially. --- cparser/Lexer.mll | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 881d411a..bce0e504 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -95,7 +95,8 @@ let () = (* We can ignore the __extension__ GCC keyword. *) ignored_keywords := SSet.add "__extension__" !ignored_keywords -let init_ctx = SSet.singleton "__builtin_va_list" +let init_ctx = SSet.of_list (List.map fst CBuiltins.builtins.C.builtin_typedefs) + let types_context : SSet.t ref = ref init_ctx let _ = -- cgit From c50680bb86564fe61db61e6140a418ccc7d36677 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 15:54:51 +0100 Subject: AArch64: macOS port This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors. --- cparser/Machine.ml | 3 +++ cparser/Machine.mli | 1 + 2 files changed, 4 insertions(+) (limited to 'cparser') diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 97bedb3b..43b6351b 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -242,6 +242,9 @@ let aarch64 = struct_passing_style = SP_ref_callee; (* Wrong *) struct_return_style = SR_ref } (* Wrong *) +let aarch64_apple = + { aarch64 with char_signed = true } + (* Add GCC extensions re: sizeof and alignof *) let gcc_extensions c = diff --git a/cparser/Machine.mli b/cparser/Machine.mli index ca7de17b..6d7ffbac 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -87,6 +87,7 @@ val arm_bigendian : t val rv32 : t val rv64 : t val aarch64 : t +val aarch64_apple : t val gcc_extensions : t -> t val compcert_interpreter : t -> t -- cgit From 35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 3 Jan 2021 16:01:20 +0100 Subject: Ignore and warn about pragmas inside functions Pragmas can occur either outside external declarations, at the top level of a compilation unit, or within a compound statement, inside a function definition. The parse tree in cparse/C.mli cannot represent pragmas occuring within a compound statement. In this case, the elaborator used to silently move the pragma to top level, just before the function definition where the pragma occurs. It looks safer to just ignore pragmas occurring inside a function definition, and emit a specific warning. --- cparser/Elab.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bb9f8aca..2e02275c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2871,7 +2871,10 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (* pragma *) | PRAGMA(s, loc) -> - emit_elab env loc (Gpragma s); + if local then + warning loc Unknown_pragmas "pragmas are ignored inside functions" + else + emit_elab env loc (Gpragma s); ([], env) (* static assertion *) -- cgit From 6bef869040014b4d589a8e49b42ac36a970d1bc6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 16 Jan 2021 10:27:49 +0100 Subject: Change warning for pragmas inside functions Follow-up to 35e2b11db. Put the warning "pragmas are ignored inside functions" inside the Unnamed category, so that it is displayed by default and cannot be disabled. --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2e02275c..25e4a980 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2872,7 +2872,7 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (* pragma *) | PRAGMA(s, loc) -> if local then - warning loc Unknown_pragmas "pragmas are ignored inside functions" + warning loc Unnamed "pragmas are ignored inside functions" else emit_elab env loc (Gpragma s); ([], env) -- cgit From ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 18 Jan 2021 19:56:44 +0100 Subject: "macosx" is now called "macos" The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos". --- cparser/Machine.ml | 4 ++-- cparser/Machine.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'cparser') diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 43b6351b..8de4ed07 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -178,12 +178,12 @@ let x86_32 = struct_passing_style = SP_split_args; struct_return_style = SR_ref} -let x86_32_macosx = +let x86_32_macos = {x86_32 with struct_passing_style = SP_split_args; struct_return_style = SR_int1248 } let x86_32_bsd = - x86_32_macosx + x86_32_macos let x86_64 = { i32lpll64 with name = "x86_64"; char_signed = true; diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 6d7ffbac..aa99f1aa 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -71,7 +71,7 @@ val ilp32ll64 : t val i32lpll64 : t val il32pll64 : t val x86_32 : t -val x86_32_macosx : t +val x86_32_macos : t val x86_32_bsd : t val x86_64 : t val win32 : t -- cgit