aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 14:31:06 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 14:31:06 +0100
commitba21b0ae95189f2d40cca38c502c1ca583a0e1bb (patch)
tree44ee07a6b8d8766638b2b1b5f4d1ca4364b0cf24 /cparser/Elab.ml
parent01a07b1c68f108df1376beaafdc3242b629634de (diff)
downloadcompcert-kvx-ba21b0ae95189f2d40cca38c502c1ca583a0e1bb.tar.gz
compcert-kvx-ba21b0ae95189f2d40cca38c502c1ca583a0e1bb.zip
parse _Thread_local
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3dbb9d45..b76a61cb 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -626,6 +626,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
- a set of attributes (const, volatile, restrict)
- a list of type specifiers *)
let sto = ref Storage_default
+ and thread_local = ref false
and inline = ref false
and noreturn = ref false
and restrict = ref false
@@ -645,6 +646,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
| STATIC -> sto := Storage_static
| EXTERN -> sto := Storage_extern
| REGISTER -> sto := Storage_register
+ | THREAD_LOCAL -> thread_local := true
| TYPEDEF ->
if !typedef then
error loc "multiple uses of 'typedef'";