Ignore unknown pragmas during lexing (#597)

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 <bernhardschommer@gmail.com>

Author: xavierleroy

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

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 }