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, 2 deletions

diff --git a/common/Sections.ml b/common/Sections.ml
index b792581f..1c2e8291 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -189,8 +189,7 @@ let for_variable env id ty init =
 
 (* Determine sections for a function definition *)
 
-let for_function env id ty_res =
-  let attr = Cutil.attributes_of_type env ty_res in
+let for_function env id attr =
   let si_code =
     try
       (* 1- Section explicitly associated with #use_section *)