diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll index de31b52c9d6179cdb2d7fb033b4f3a3785654807..765ee47bd84fb34a4f24a9eb05c3976eb636e912 100644 --- a/src/kernel_internals/parsing/clexer.mll +++ b/src/kernel_internals/parsing/clexer.mll @@ -206,13 +206,28 @@ let init_lexicon _ = ("__builtin_va_arg", fun loc -> BUILTIN_VA_ARG loc); ("__builtin_types_compatible_p", fun loc -> BUILTIN_TYPES_COMPAT loc); ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc); - (* On some versions of GCC __thread is a regular identifier *) + ("_Thread_local", + fun loc -> + if Kernel.C11.get () then THREAD loc + else begin + Kernel.( + warning + ~wkey:wkey_conditional_feature + "_Thread_local is a C11 keyword, use -c11 option to enable it"); + IDENT "_Thread_local" + end); + (* We recognize __thread for GCC machdeps *) ("__thread", - (fun loc -> - if Cil.theMachine.Cil.theMachine.Cil_types.__thread_is_keyword then - THREAD loc - else - IDENT "__thread")); + fun loc -> + if Cil.gccMode () then + THREAD loc + else begin + Kernel.( + warning + ~wkey:wkey_conditional_feature + "__thread is a GCC extension, use a GCC-based machdep to enable it"); + IDENT "__thread" + end); ("__FC_FILENAME__", (fun loc -> let filename = diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 8613ec75b579545f53ec9600e5e5514081b87ae4..c77c2f75cdbe34e57f13140ee4f7f04c75869c70 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -1510,7 +1510,11 @@ attribute_nocv: | DECLSPEC paren_attr_list_ne { ("__declspec", $2), $1 } | MSATTR { (fst $1, []), snd $1 } /* ISO 6.7.3 */ -| THREAD { ("__thread",[]), $1 } +| THREAD { ("__thread", + if Kernel.C11.get() then [make_expr (VARIABLE "c11")] + else [] + ), $1 } + ; attribute_nocv_list: diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 085144c8958e90e32ddf4d935a75bc010c1dd2f3..4d3312bae1154f6a0a2ba915bb467a9e8db4e179 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -2056,6 +2056,9 @@ class cil_printer () = object (self) | "const", [] -> self#pp_keyword fmt "const"; false (* Put the aconst inside the attribute list *) | "aconst", [] when not (Cil.msvcMode ()) -> fprintf fmt "__const__"; true + | "thread", [ ACons ("c11",[]) ] + when not state.print_cil_as_is -> + fprintf fmt "_Thread_local"; false | "thread", [] when not (Cil.msvcMode ()) -> fprintf fmt "__thread"; false | "volatile", [] -> self#pp_keyword fmt "volatile"; false | "ghost", [] -> self#pp_keyword fmt "\\ghost"; false diff --git a/tests/syntax/oracle/thread.res.oracle b/tests/syntax/oracle/thread.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..1d65cdc4dc26f609ee94fe672ffafea4013325ca --- /dev/null +++ b/tests/syntax/oracle/thread.res.oracle @@ -0,0 +1,19 @@ +[kernel] Parsing tests/syntax/thread.i (no preprocessing) +/* Generated by Frama-C */ + _Thread_local int a; +static _Thread_local int b; +extern _Thread_local int c; + + _Thread_local int d; +int main(void) +{ + int __retres; + a = 0; + b = 0; + c = 0; + d = 0; + __retres = 0; + return __retres; +} + + diff --git a/tests/syntax/thread.i b/tests/syntax/thread.i new file mode 100644 index 0000000000000000000000000000000000000000..209b26f890d3076ac0a21216a81f48964b3be06a --- /dev/null +++ b/tests/syntax/thread.i @@ -0,0 +1,16 @@ +/* run.config + STDOPT: +"-machdep gcc_x86_32 -c11" + */ + +__thread int a; +static __thread int b; +extern __thread int c; +_Thread_local int d; + +int main() { + a = 0; + b = 0; + c = 0; + d = 0; + return 0; +}