aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Cleanup.ml2
-rw-r--r--cparser/Elab.ml1
-rw-r--r--cparser/Rename.ml7
3 files changed, 7 insertions, 3 deletions
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index b15e150c..9f19395a 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -126,7 +126,7 @@ let add_enum e =
*)
let visible_decl (sto, id, ty, init) =
- sto = Storage_default &&
+ (sto = Storage_default || sto = Storage_thread_local) &&
match ty with TFun _ -> false | _ -> true
let visible_fundef f =
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index a428d17c..42505a2c 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -674,6 +674,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
error loc "_Thread_local on auto or register variable";
!sto
)
+
| TYPEDEF ->
if !typedef then
error loc "multiple uses of 'typedef'";
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 64412194..aeeb9326 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -257,13 +257,16 @@ let rec reserve_public env = function
match dcl.gdesc with
| Gdecl(sto, id, _, _) ->
begin match sto with
- | Storage_default | Storage_extern -> enter_public env id
+ | Storage_default | Storage_thread_local
+ | Storage_extern | Storage_thread_local_extern ->
+ enter_public env id
| Storage_static -> env
| _ -> assert false
end
| Gfundef f ->
begin match f.fd_storage with
- | Storage_default | Storage_extern -> enter_public env f.fd_name
+ | Storage_default | Storage_extern
+ -> enter_public env f.fd_name
| Storage_static -> env
| _ -> assert false
end