diff options
| author | Michael Schmidt <github@mschmidt.me> | 2018-04-09 13:51:43 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2018-04-25 16:39:43 +0200 |
| commit | 3b6a054a9a2f54e9c351a4d343331499453c39c5 (patch) | |
| tree | 5d2fc35a70be70d694c02b1c5757eb96d5f8b004 /cparser/Elab.ml | |
| parent | 92c8be3a36dff49f92e6cf94719a1750e4961538 (diff) | |
| download | compcert-kvx-3b6a054a9a2f54e9c351a4d343331499453c39c5.tar.gz compcert-kvx-3b6a054a9a2f54e9c351a4d343331499453c39c5.zip | |
Add diagnostic for illegal use of void (Bug 23342)
Diffstat (limited to 'cparser/Elab.ml')
| -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 66078585..54021ee4 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -750,6 +750,8 @@ and elab_parameter keep_ty env (PARAM (spec, id, decl, attr, loc)) = if noret then error loc "'_Noreturn' can only appear on functions"; let id = match id with None -> "" | Some id -> id in + if id <> "" && is_void_type env1 ty then + error loc "argument '%s' may not have 'void' type" id; if id <> "" && redef Env.lookup_ident env id then error loc "redefinition of parameter '%s'" id; (* replace array and function types by pointer types *) |