Merge of the "alignas" branch.

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

2 files changed, 27 insertions, 14 deletions

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 1cb93d5..246e12c 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.
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 9027f86..8c83fab 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -137,10 +137,15 @@ let coqint64 p n =
 let use_struct_names = ref true
 
 let rec typ p t =
-  let a = attr_of_type t in
-  if a (*.attr_volatile*)
-  then fprintf p "(tvolatile %a)" rtyp t
-  else rtyp p t
+  match attr_of_type t with
+  | { attr_volatile = false; attr_alignas = None} ->
+        rtyp p t
+  | { attr_volatile = true; attr_alignas = None} ->
+        fprintf p "(tvolatile %a)" rtyp t
+  | { attr_volatile = false; attr_alignas = Some n} ->
+        fprintf p "(talignas %ld%%N %a)" (N.to_int32 n) rtyp t
+  | { attr_volatile = true; attr_alignas = Some n} ->
+        fprintf p "(tvolatile_alignas %ld%%N %a)" (N.to_int32 n) rtyp t
 
 and rtyp p = function
   | Tvoid -> fprintf p "tvoid"