diff options
Diffstat (limited to 'cparser')
| -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 *) |