From a6c369cbd63996c1571ae601b7d92070f024b22c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 5 Oct 2013 08:11:34 +0000
Subject: Merge of the "alignas" branch.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 exportclight/Clightdefs.v    | 28 ++++++++++++++++++----------
 exportclight/ExportClight.ml | 13 +++++++++----
 2 files changed, 27 insertions(+), 14 deletions(-)

(limited to 'exportclight')

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.
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 9027f86d..8c83fabb 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"
-- 
cgit