diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-18 09:46:23 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-18 09:46:23 +0200 |
| commit | f26267c6289e4fa306a0875ff149a00ee401e043 (patch) | |
| tree | dd7dbc39fb89fd0e08bf39ef7683950ad7303c4a /cparser | |
| parent | e2b4459ccd1b0f8436cb70a631772d715e642dcd (diff) | |
| download | compcert-f26267c6289e4fa306a0875ff149a00ee401e043.tar.gz compcert-f26267c6289e4fa306a0875ff149a00ee401e043.zip | |
Disallow void as type for variables.
This allows problems in elaboration of the initializers for
variables of void type.
Bug 19577.
Diffstat (limited to 'cparser')
| -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 8cd7ed64..2b5b4591 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1942,6 +1942,8 @@ let enter_decdefs local loc env sto dl = initializer can refer to the ident *) let (id, sto', env1, ty, linkage) = enter_or_refine_ident local loc env s sto1 ty in + if not isfun && is_void_type env ty then + fatal_error loc "'%s' has incomplete type" s; (* process the initializer *) let (ty', init') = elab_initializer loc env1 s ty init in (* update environment with refined type *) |