diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
| commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
| tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /cparser | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
| download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip | |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
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 |