diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-04-26 18:05:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-04-26 18:05:52 +0200 |
| commit | 83f812f9cee254606f96244a7808869b7802f309 (patch) | |
| tree | d1248a4e9fc855281eeb24f1fb0594313993e8ca | |
| parent | f1d9a90486ac2744e0f2096eeaeedac117af5b9a (diff) | |
| download | compcert-kvx-83f812f9cee254606f96244a7808869b7802f309.tar.gz compcert-kvx-83f812f9cee254606f96244a7808869b7802f309.zip | |
Additional checks on typedefs (#101)
Typedefs should have a name and also should not contain _Noreturn.
Bug 23381
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index dddbd03b..c561c057 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -792,6 +792,8 @@ and elab_name_group keep_ty loc env (spec, namelist) = and elab_init_name_group keep_ty loc env (spec, namelist) = let (sto, inl, noret, tydef, bty, env') = elab_specifier keep_ty ~only:(namelist=[]) loc env spec in + if noret && tydef then + error loc "'_Noreturn' can only appear on functions"; let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = let ((ty, _), env1) = elab_type_declarator keep_ty loc env bty false decl in @@ -2180,6 +2182,8 @@ let __func__type_and_init s = let enter_typedefs loc env sto dl = if sto <> Storage_default then error loc "non-default storage class on 'typedef' definition"; + if dl = [] then + warning loc Missing_declarations "typedef requires a name"; List.fold_left (fun env (s, ty, init) -> if init <> NO_INIT then error loc "initializer in typedef"; |