From 205533e810539b0b96835db560957c31cf87ee68 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 26 May 2020 10:53:30 +0200
Subject: [PATCH] [Parsing] accept C11's _Thread_local
---
src/kernel_internals/parsing/clexer.mll | 27 ++++++++++++++-----
src/kernel_internals/parsing/cparser.mly | 6 ++++-
.../ast_printing/cil_printer.ml | 3 +++
tests/syntax/oracle/thread.res.oracle | 19 +++++++++++++
tests/syntax/thread.i | 16 +++++++++++
5 files changed, 64 insertions(+), 7 deletions(-)
create mode 100644 tests/syntax/oracle/thread.res.oracle
create mode 100644 tests/syntax/thread.i
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index de31b52c9d6..765ee47bd84 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 8613ec75b57..c77c2f75cdb 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 085144c8958..4d3312bae11 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 00000000000..1d65cdc4dc2
--- /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 00000000000..209b26f890d
--- /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;
+}
--
GitLab