diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-04-19 07:55:04 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-04-19 08:55:04 +0300 |
| commit | e79bc7f63db91866c2401c898cffe373125d46c6 (patch) | |
| tree | 3f30b60654ae4d9b1dcd921dd65c64301a1b19ab /cparser/Elab.ml | |
| parent | 9195d4826485709c1a903ab307b7e18112c021ab (diff) | |
| download | compcert-kvx-e79bc7f63db91866c2401c898cffe373125d46c6.tar.gz compcert-kvx-e79bc7f63db91866c2401c898cffe373125d46c6.zip | |
Function defintions: keep the attributes from previous declarations (#89)
After calling enter_or_refine for a function identifier we need to keep
the combined attributes. Here is an example where it makes a difference:
```
_Noreturn void f(int x);
void f(int x) { }
```
Before this commit, the `_Noreturn` on the declaration is ignored when checking the definition.
Bug 23385
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 88262421..074779ca 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2367,8 +2367,10 @@ let elab_fundef env spec name defs body loc = | _ -> fatal_error loc "wrong type for function definition" in (* Enter function in the environment, for recursive references *) add_global_define loc s; - let (fun_id, sto1, env1, _, _) = + let (fun_id, sto1, env1, new_ty, _) = enter_or_refine_ident false loc env1 s sto ty in + (* Take into account attributes from previous declarations of the function *) + let attr = attributes_of_type env1 new_ty in let incomplete_param env ty = if wrap incomplete_type loc env ty then fatal_error loc "parameter has incomplete type" in |