aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-08-17 13:59:17 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-08-17 13:59:17 +0200
commit11837beafc84f226878b4706a791e9c13301e01f (patch)
tree62a1ac44f08ff0712d72566c3c6c257be515948f /cparser/Elab.ml
parent44c859e5ffd95498b6e0dc504a9fc54cef86aae8 (diff)
downloadcompcert-kvx-11837beafc84f226878b4706a791e9c13301e01f.tar.gz
compcert-kvx-11837beafc84f226878b4706a791e9c13301e01f.zip
Added a check for parameters without identifiers. (#128)
It is not allowed in C to have a parameter in a parameter list without an identifier. Bug 24283
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml12
1 files changed, 7 insertions, 5 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index cff9ed5b..173d3e03 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2519,9 +2519,13 @@ let elab_fundef genv spec name defs body loc =
(* Take into account attributes from previous declarations of the function *)
let attr = attributes_of_type genv new_ty in
(* Additional checks on function parameters *)
- let incomplete_param env ty =
+ let add_param env (id, ty) =
if wrap incomplete_type loc env ty then
- fatal_error loc "parameter has incomplete type" in
+ fatal_error loc "parameter has incomplete type";
+ if id.C.name = "" then
+ error loc "parameter name omitted";
+ Env.add_ident env id Storage_default ty
+ in
(* Enter parameters and extra declarations in the local environment.
For K&R functions this hasn't been done yet.
For prototyped functions this has been done by [elab_fundef_name]
@@ -2531,9 +2535,7 @@ let elab_fundef genv spec name defs body loc =
parameter [f] and not to the function [f] within the body of the
function. *)
let lenv =
- List.fold_left (fun e (id, ty) -> incomplete_param e ty;
- Env.add_ident e id Storage_default ty)
- lenv params in
+ List.fold_left add_param lenv params in
let lenv =
List.fold_left (fun e (sto, id, ty, init) -> Env.add_ident e id sto ty)
lenv extra_decls in