diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-05-04 16:18:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-05-04 16:18:11 +0200 |
| commit | 338bbeace6ee351962e42172fd7c7acbcf5e785c (patch) | |
| tree | dd5f4b8231bdc71af968c672a74a8b53b40658a8 /cparser/Elab.ml | |
| parent | e224022a4887029ed099a265a8e3c71c84d67556 (diff) | |
| download | compcert-kvx-338bbeace6ee351962e42172fd7c7acbcf5e785c.tar.gz compcert-kvx-338bbeace6ee351962e42172fd7c7acbcf5e785c.zip | |
Reject empty declarations in K&R functions. (#107)
Empty declarations in K&R function parameters are not allowed
by the C standard.
Bug 23375
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1b87c095..7e029312 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2301,6 +2301,8 @@ let elab_KR_function_parameters env params defs loc = let elab_param_def env = function | DECDEF((spec', name_init_list), loc') -> let name_list = List.map extract_name name_init_list in + if name_list = [] then + error loc' "declaration does not declare a parameter"; let (paramsenv, sto) = elab_name_group true loc' env (spec', name_list) in if sto <> Storage_default && sto <> Storage_register then error loc' (* NB: 'auto' not allowed *) |