diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-11 13:05:58 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-11 13:05:58 +0100 |
commit | fd2d8d86daf9d63d5695c93f412a7cf549d312c6 (patch) | |
tree | e44d0c6afed8cb09f244626b96df71e084a070ec /cparser/Lexer.mll | |
parent | da4ca8a5313c6dc1f6015102b42dfbbeeb546dc7 (diff) | |
download | compcert-fd2d8d86daf9d63d5695c93f412a7cf549d312c6.tar.gz compcert-fd2d8d86daf9d63d5695c93f412a7cf549d312c6.zip |
More gcc/newlib compatibility code.
Some newlib headers use the __extension__ keyword which suppresses
warnings for gcc extensions in strict mode. CompCert now ignores
this keyword for the gnu backends.
Also it seems that stddef of the gcc defines wint_t even though
it should not. However some libs rely on this. So wint_t is now
defined in CompCert's stddef header.
Bug 17613.
Diffstat (limited to 'cparser/Lexer.mll')
-rw-r--r-- | cparser/Lexer.mll | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 6fac15e8..bcf2ada0 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -23,6 +23,7 @@ open Camlcoq module SSet = Set.Make(String) let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl.create 17 +let ignored_keyworkds : SSet.t ref = ref SSet.empty let () = List.iter (fun (key, builder) -> Hashtbl.add lexicon key builder) @@ -81,7 +82,10 @@ let () = ("unsigned", fun loc -> UNSIGNED loc); ("void", fun loc -> VOID loc); ("volatile", fun loc -> VOLATILE loc); - ("while", fun loc -> WHILE loc)] + ("while", fun loc -> WHILE loc)]; + if Configuration.system <> "diab" then + (* We can ignore the __extension__ GCC keyword. *) + ignored_keyworkds := SSet.add "__extension__" !ignored_keyworkds let init_ctx = SSet.singleton "__builtin_va_list" let types_context : SSet.t ref = ref init_ctx @@ -325,6 +329,9 @@ rule initial = parse | "," { COMMA(currentLoc lexbuf) } | "." { DOT(currentLoc lexbuf) } | identifier as id { + if SSet.mem id !ignored_keyworkds then + initial lexbuf + else try Hashtbl.find lexicon id (currentLoc lexbuf) with Not_found -> PRE_NAME id } | eof { EOF } |