Merge of the "alignas" branch.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 18 insertions, 10 deletions

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 1cb93d54..246e12c1 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -39,18 +39,26 @@ Definition tdouble := Tfloat F64 noattr.
 Definition tptr (t: type) := Tpointer t noattr.
 Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
 
-Definition volatile_attr := {| attr_volatile := true |}.
+Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}.
 
-Definition tvolatile (ty: type) :=
+Definition tattr (a: attr) (ty: type) :=
   match ty with
   | Tvoid => Tvoid
-  | Tint sz si a => Tint sz si volatile_attr
-  | Tlong si a => Tlong si volatile_attr
-  | Tfloat sz a => Tfloat sz volatile_attr
-  | Tpointer elt a => Tpointer elt volatile_attr
-  | Tarray elt sz a => Tarray elt sz volatile_attr
+  | Tint sz si _ => Tint sz si a
+  | Tlong si _ => Tlong si a
+  | Tfloat sz _ => Tfloat sz a
+  | Tpointer elt _ => Tpointer elt a
+  | Tarray elt sz _ => Tarray elt sz a
   | Tfunction args res => Tfunction args res 
-  | Tstruct id fld a => Tstruct id fld volatile_attr
-  | Tunion id fld a => Tunion id fld volatile_attr
-  | Tcomp_ptr id a => Tcomp_ptr id volatile_attr
+  | Tstruct id fld _ => Tstruct id fld a
+  | Tunion id fld _ => Tunion id fld a
+  | Tcomp_ptr id _ => Tcomp_ptr id a
   end.
+
+Definition tvolatile (ty: type) := tattr volatile_attr ty.
+
+Definition talignas (n: N) (ty: type) :=
+  tattr {| attr_volatile := false; attr_alignas := Some n |} ty.
+
+Definition tvolatile_alignas (n: N) (ty: type) :=
+  tattr {| attr_volatile := true; attr_alignas := Some n |} ty.