Revised elaboration of attributes

The treatment of attributes in the current CompCert is often surprising.  For example,

   attribute(xxx) char * x;

is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char".

CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e.

   const char * x;

is really "x is a pointer to a const char", not "x is a const pointer to char".

This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes.  The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined.  In the examples above,

   attribute(xxx) char * x;    // "attribute(xxx)" applies to "x"
   const char * x;             // "const" applies to "char"

This may be a step in the right direction but is not the final story.  In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.

1 files changed, 1 insertions, 1 deletions

diff --git a/common/Sections.mli b/common/Sections.mli
index 8a13fb8a..b83b0bb4 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -47,5 +47,5 @@ val use_section_for: AST.ident -> string -> bool
 
 val for_variable: Env.t -> AST.ident -> C.typ -> bool ->
                                           section_name * access_mode
-val for_function: Env.t -> AST.ident -> C.typ -> section_name list
+val for_function: Env.t -> AST.ident -> C.attributes -> section_name list
 val for_stringlit: unit -> section_name