aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-08-20 10:17:57 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2018-08-20 10:17:57 +0200
commitec8d93afc8875dcf7dfeb982eab255f150a91074 (patch)
tree80f1f2b22b2f9904346dc6b8ece81cce51289792 /cparser/Elab.ml
parenta40a2797d80d510bcd36bb72cf3eafba4cee1bd5 (diff)
downloadcompcert-kvx-ec8d93afc8875dcf7dfeb982eab255f150a91074.tar.gz
compcert-kvx-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
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml6
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.