- Support for _Alignof(ty) operator from ISO C 2011

  and __alignof__(ty), __alignof__(expr) from GCC.
- Resurrected __builtin_memcpy_aligned, useful for files generated
  by Scade KCG 6.



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

1 files changed, 2 insertions, 0 deletions

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ffe08bfa..e9e260bd 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -210,6 +210,7 @@ Inductive expr : Type :=
   | Ecast (r: expr) (ty: type)                        (**r type cast [(ty)r] *)
   | Econdition (r1 r2 r3: expr) (ty: type)  (**r conditional [r1 ? r2 : r3] *)
   | Esizeof (ty': type) (ty: type)                      (**r size of a type *)
+  | Ealignof (ty': type) (ty: type)        (**r natural alignment of a type *)
   | Eassign (l: expr) (r: expr) (ty: type)          (**r assignment [l = r] *)
   | Eassignop (op: binary_operation) (l: expr) (r: expr) (tyres ty: type)
                                   (**r assignment with arithmetic [l op= r] *)
@@ -296,6 +297,7 @@ Definition typeof (a: expr) : type :=
   | Ecast _ ty => ty
   | Econdition _ _ _ ty => ty
   | Esizeof _ ty => ty
+  | Ealignof _ ty => ty
   | Eassign _ _ ty => ty
   | Eassignop _ _ _ _ ty => ty
   | Epostincr _ _ ty => ty