From a6c369cbd63996c1571ae601b7d92070f024b22c Mon Sep 17 00:00:00 2001 From: xleroy 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 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'exportclight/Clightdefs.v') 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. -- cgit