diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-20 16:22:36 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-20 16:22:36 +0200 |
| commit | 3e1ceff43f0c636136d333dd8bf7214bf3798fea (patch) | |
| tree | e66db545c2688f9db34b54e97aea94e3800d5825 /cparser | |
| parent | 98427e8d2e51b1b7590bbde3fc18c49ff7dd8e13 (diff) | |
| download | compcert-3e1ceff43f0c636136d333dd8bf7214bf3798fea.tar.gz compcert-3e1ceff43f0c636136d333dd8bf7214bf3798fea.zip | |
Added check for incomplete parameter types.
Parameters also need to be checked for incomplete types.
Bug 19596
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 973dfb30..eeff41e1 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2105,9 +2105,13 @@ let elab_fundef env spec name defs body loc = (* Enter function in the environment, for recursive references *) let (fun_id, sto1, env1, _, _) = enter_or_refine_ident false loc env1 s sto ty in + let incomplete_param env ty = + if wrap incomplete_type loc env ty then + fatal_error loc "parameter has incomplete type" in (* Enter parameters and extra declarations in the environment *) let env2 = - List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) + List.fold_left (fun e (id, ty) -> incomplete_param e ty; + Env.add_ident e id Storage_default ty) (Env.new_scope env1) params in let env2 = List.fold_left (fun e (sto, id, ty, init) -> Env.add_ident e id sto ty) |