diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-09-03 13:11:02 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-09-03 13:11:02 +0200 |
| commit | 3389bd5b2b7875243738afeb28109bfc5a5a853d (patch) | |
| tree | 38c4a761fdf12b6d998d91f9660f805a65881e48 | |
| parent | b4b1fa3d47c37829be30367ced9aa89abcd7f5c7 (diff) | |
| download | compcert-3389bd5b2b7875243738afeb28109bfc5a5a853d.tar.gz compcert-3389bd5b2b7875243738afeb28109bfc5a5a853d.zip | |
Move parameter check.
Instead of performing the check only for parameters of function
definitions also perform it for function declarations.
Bug 23393
| -rw-r--r-- | cparser/Elab.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1c6bbebf..146cab2e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -871,6 +871,12 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = let ty1 = argument_conversion env1 ty in if is_qualified_array ty1 then error loc "type qualifier used in non-outermost array type derivation"; + if has_std_alignas (attributes_of_type env ty) then begin + if id <> "" then + error loc "alignment specified for parameter '%s'" id + else + error loc "alignment specified for unnamed parameter" + end; let (id', env2) = Env.enter_ident env1 id sto ty1 in ( (id', ty1) , env2) @@ -2616,8 +2622,6 @@ let elab_fundef genv spec name defs body loc = fatal_error loc "parameter has incomplete type"; if id.C.name = "" then fatal_error loc "parameter name omitted"; - if has_std_alignas (attributes_of_type env ty) then - error loc "alignment specified for parameter '%s'" id.C.name; Env.add_ident env id Storage_default ty in (* Enter parameters and extra declarations in the local environment. |