diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-06-03 10:12:48 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-06-03 10:12:48 +0200 |
| commit | 37bc5d7c21278a0f5cab9a2f61bdacd7f5a4d4fb (patch) | |
| tree | 182faf24e22630404c8678aea605be08e1846626 | |
| parent | 8b0724fdb1af4f89a603f7bde4b5b625c870e111 (diff) | |
| download | compcert-37bc5d7c21278a0f5cab9a2f61bdacd7f5a4d4fb.tar.gz compcert-37bc5d7c21278a0f5cab9a2f61bdacd7f5a4d4fb.zip | |
New additional check for void parameters. (#174)
There should only be one unnamed parameter of type void in the
parameter list.
| -rw-r--r-- | cparser/Elab.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 9cca930d..10380152 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -836,7 +836,7 @@ and elab_type_declarator ?(fundef = false) loc env ty = function | Cabs.PROTO(d, (params, vararg)) -> elab_return_type loc env ty; let (ty, a) = get_nontype_attrs env ty in - let (params', env') = elab_parameters env params in + let (params', env') = elab_parameters loc env params in (* For a function declaration (fundef = false), the scope introduced to treat parameters ends here, so we discard the extended environment env' returned by elab_parameters. @@ -862,13 +862,15 @@ and elab_type_declarator ?(fundef = false) loc env ty = function (* Elaboration of parameters in a prototype *) -and elab_parameters env params = +and elab_parameters loc env params = (* Prototype introduces a new scope *) let (vars, env) = mmap elab_parameter (Env.new_scope env) params in (* Catch special case f(t) where t is void or a typedef to void *) match vars with | [ ( {C.name=""}, t) ] when is_void_type env t -> [],env - | _ -> vars,env + | _ -> if List.exists (fun (id, t) -> id.C.name = "" && is_void_type env t) vars then + error loc "'void' must be the only parameter"; + (vars, env) (* Elaboration of a function parameter *) |