From 53a5fc35ed8cf6e1ad9d9e2b760ee9e8150d48e1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 12 Sep 2026 14:41:58 +0200 Subject: [PATCH] Ignore unknown pragmas during lexing Currently, the parser accepts `#pragma` directives that occur in declaration position. Elab ignores (with a warning) pragmas that are not global declarations. C2C ignores (with a warning) all remaining pragmas except the `section`, `use_section` and `reserve_register` pragmas handled in cfrontend/CPragmas.ml. However, `#pragma` directives can occur anywhere in a C source file, incl. in the middle of a statement or an expression. Some system header files includes such weird pragmas. This PR recognizes `#pragma` directives that are not handled in cfrontend/CPragmas.ml during lexical analysis and ignores them (with a warning). No `PRAGMA` token is generated for unhandled pragmas. This way, unhandled pragmas can occur anywhere in the source file and will not cause parsing errors. Co-authored-by: Bernhard Schommer --- cfrontend/CPragmas.ml | 6 ++++++ cparser/Lexer.mll | 11 ++++++++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 08d0aa6c91..571de6cd62 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -87,8 +87,14 @@ let process_pragma name = | _ -> false +let supported_pragma name = + match Tokenize.string name with + | ("section" | "use_section" | "reserve_register") :: _ -> true + | _ -> false + let reset () = reserved_registers := [] let initialize () = + Lexer.supported_pragma := supported_pragma; C2C.process_pragma_hook := process_pragma diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 099c218473..74c72186ab 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -99,6 +99,8 @@ let () = (* We can ignore the __extension__ GCC keyword. *) ignored_keywords := SSet.add "__extension__" !ignored_keywords +let supported_pragma : (string -> bool) ref = ref (fun _ -> false) + let init_ctx = SSet.of_list (List.map fst CBuiltins.builtins.C.builtin_typedefs) let types_context : SSet.t ref = ref init_ctx @@ -528,7 +530,14 @@ and hash = parse "pragma" whitespace_char_no_newline + ([^ '\n']* as s) '\n' - { new_line lexbuf; PRAGMA (s, currentLoc lexbuf) } + { if !supported_pragma s then begin + new_line lexbuf; + PRAGMA (s, currentLoc lexbuf) + end else begin + warning lexbuf Diagnostics.Unknown_pragmas "unknown pragma ignored"; + new_line lexbuf; + initial_linebegin lexbuf + end } | [^ '\n']* '\n' { warning lexbuf Diagnostics.Unnamed "unrecognized '#' line"; new_line lexbuf; initial_linebegin lexbuf }