diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 5 | ||||
| -rw-r--r-- | cparser/Lexer.mll | 3 | ||||
| -rw-r--r-- | cparser/Machine.ml | 7 | ||||
| -rw-r--r-- | cparser/Machine.mli | 3 |
4 files changed, 13 insertions, 5 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index e822dfcb..46163104 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2901,7 +2901,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 Unnamed "pragmas are ignored inside functions" + else + emit_elab env loc (Gpragma s); ([], env) (* static assertion *) diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index f5e8edb3..d20ac50e 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -96,7 +96,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 _ = diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 73b71ea0..36a6c023 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -183,12 +183,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; @@ -283,6 +283,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 54436758..5bf95bb6 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -73,7 +73,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 @@ -90,6 +90,7 @@ val rv32 : t val rv64 : t val kvx : t val aarch64 : t +val aarch64_apple : t val gcc_extensions : t -> t val compcert_interpreter : t -> t |