diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 16:01:35 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 16:01:35 +0100 |
| commit | 9d4d852eb960926453f216722f629d3c8dc9cf13 (patch) | |
| tree | b0419ac4ab0009b1477a526ee73dee897b73ce6a /cparser | |
| parent | 034eff1d4d4f168008cded71b73bd39066b97997 (diff) | |
| download | compcert-kvx-9d4d852eb960926453f216722f629d3c8dc9cf13.tar.gz compcert-kvx-9d4d852eb960926453f216722f629d3c8dc9cf13.zip | |
actually process the modifiers
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 98f88dc9..a428d17c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -643,7 +643,6 @@ 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 @@ -663,7 +662,18 @@ 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 + | THREAD_LOCAL -> + sto := (match !sto with + | Storage_static | Storage_thread_local_static -> + Storage_thread_local_static + | Storage_extern | Storage_thread_local_extern -> + Storage_thread_local_extern + | Storage_default | Storage_thread_local -> + Storage_thread_local + | Storage_auto|Storage_register -> + error loc "_Thread_local on auto or register variable"; + !sto + ) | TYPEDEF -> if !typedef then error loc "multiple uses of 'typedef'"; |