diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-08-20 10:17:57 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-08-20 10:17:57 +0200 |
| commit | ec8d93afc8875dcf7dfeb982eab255f150a91074 (patch) | |
| tree | 80f1f2b22b2f9904346dc6b8ece81cce51289792 | |
| parent | a40a2797d80d510bcd36bb72cf3eafba4cee1bd5 (diff) | |
| download | compcert-ec8d93afc8875dcf7dfeb982eab255f150a91074.tar.gz compcert-ec8d93afc8875dcf7dfeb982eab255f150a91074.zip | |
Turn error into fatal error for unnamed parameter.
Since the parameter name gets used in other error messages it
results in messages without names.
Bug 24283
| -rw-r--r-- | cparser/Elab.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 6b2db3da..9bce4da9 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2539,12 +2539,14 @@ let elab_fundef genv spec name defs body loc = let lenv = Env.add_ident lenv fun_id sto new_ty in (* Take into account attributes from previous declarations of the function *) let attr = attributes_of_type genv new_ty in - (* Additional checks on function parameters *) + (* Additional checks on function parameters. They should have a complete type + and additionally they should have an identifier. In both cases a fatal + error is raised in order to avoid problems at later places. *) let add_param env (id, ty) = if wrap incomplete_type loc env ty then fatal_error loc "parameter has incomplete type"; if id.C.name = "" then - error loc "parameter name omitted"; + fatal_error loc "parameter name omitted"; Env.add_ident env id Storage_default ty in (* Enter parameters and extra declarations in the local environment. |