From e79bc7f63db91866c2401c898cffe373125d46c6 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 19 Apr 2018 07:55:04 +0200 Subject: 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 --- cparser/Elab.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- cgit