diff options
| -rw-r--r-- | cparser/Lexer.mll | 9 | ||||
| -rw-r--r-- | runtime/include/stddef.h | 15 |
2 files changed, 21 insertions, 3 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 } diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 31edf4ef..f61e87b4 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -13,7 +13,7 @@ * * Neither the name of the <organization> nor the * names of its contributors may be used to endorse or promote products * derived from this software without specific prior written permission. - * + * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -90,6 +90,18 @@ typedef signed int wchar_t; #endif #endif +#if defined (__need_wint_t) +#ifndef _WINT_T +#define _WINT_T + +#ifndef __WINT_TYPE__ +#define __WINT_TYPE__ unsigned int +#endif +typedef __WINT_TYPE__ wint_t; +#endif +#undef __need_wint_t +#endif + #if defined(_STDDEF_H) || defined(__need_NULL) #ifndef NULL #define NULL 0 @@ -102,4 +114,3 @@ typedef signed int wchar_t; #endif #endif - |