diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index f18d1b2d9f..d014921a24 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -92,6 +92,7 @@ type warning_type =
   | Unused_parameter
   | Wrong_ais_parameter
   | Unused_ais_parameter
+  | Ignored_attributes
 
 (* List of active warnings *)
 let active_warnings: warning_type list ref = ref [
@@ -114,6 +115,7 @@ let active_warnings: warning_type list ref = ref [
   Inline_asm_sdump;
   Wrong_ais_parameter;
   Unused_ais_parameter;
+  Ignored_attributes;
 ]
 
 (* List of errors treated as warning *)
@@ -145,6 +147,7 @@ let string_of_warning = function
   | Unused_parameter -> "unused-parameter"
   | Wrong_ais_parameter -> "wrong-ais-parameter"
   | Unused_ais_parameter -> "unused-ais-parameter"
+  | Ignored_attributes -> "ignored-attributes"
 
 (* Activate the given warning *)
 let activate_warning w () =
@@ -192,6 +195,7 @@ let wall () =
     Unused_variable;
     Unused_parameter;
     Wrong_ais_parameter;
+    Ignored_attributes;
   ]
 
 let wnothing () =
@@ -223,6 +227,7 @@ let werror () =
     Unused_variable;
     Wrong_ais_parameter;
     Unused_ais_parameter;
+    Ignored_attributes;
   ]
 
 (* Generate the warning key for the message *)
@@ -401,6 +406,7 @@ let warning_options =
   error_option Unused_parameter @
   error_option Wrong_ais_parameter @
   error_option Unused_ais_parameter @
+  error_option Ignored_attributes @
   [Exact ("-Wfatal-errors"), Set error_fatal;
    Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
    Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 75865cb270..ea8f215911 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -49,6 +49,7 @@ type warning_type =
   | Unused_parameter               (** unused function parameter *)
   | Wrong_ais_parameter            (** wrong parameter type for ais replacement *)
   | Unused_ais_parameter           (** unused builtin ais parameter *)
+  | Ignored_attributes             (** attributes declarations after definition *)
 
 val warning  : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
 (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index a155c893dd..52cb9ddece 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -80,6 +80,9 @@ let add_global_define loc name =
     error loc "redefinition of '%s'" name;
   global_defines := StringSet.add name !global_defines
 
+let is_global_defined name =
+  StringSet.mem name !global_defines
+
 let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td =
   let loc = elab_loc loc in
   let dec ={ gdesc = td; gloc = loc } in
@@ -153,6 +156,12 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty =
           "redefinition of '%s' with a different type: %a vs %a"
           s (print_typ env) old_ty (print_typ env) ty;
         ty in
+  if is_global_defined s then begin
+    let old_attrs = attributes_of_type env old_ty
+    and new_attrs = attributes_of_type env ty in
+    if not (Cutil.incl_attributes new_attrs old_attrs) then
+      warning loc  Ignored_attributes "attribute declaration must precede definition"
+  end;
   let new_sto =
     (* The only case not allowed is removing static *)
     match old_sto,sto with
@@ -2238,10 +2247,10 @@ let enter_decdefs local loc env sto dl =
       else sto in
     (* enter ident in environment with declared type, because
        initializer can refer to the ident *)
-    if init <> NO_INIT && not local then
-      add_global_define loc s;
     let (id, sto', env1, ty, linkage) =
       enter_or_refine_ident local loc env s sto1 ty in
+    if init <> NO_INIT && not local then
+      add_global_define loc s;
     if not isfun && is_void_type env ty then
       fatal_error loc "'%s' has incomplete type" s;
     (* process the initializer *)
@@ -2415,9 +2424,9 @@ let elab_fundef env spec name defs body loc =
         (ty_ret, params, vararg, attr)
     | _ -> 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, new_ty, _) =
     enter_or_refine_ident false loc env1 s sto ty in
+  add_global_define loc s;
   (* Take into account attributes from previous declarations of the function *)
   let attr = attributes_of_type env1 new_ty in
   let incomplete_param env ty =