From 2570ddd61b1c98b62c8d97fce862654535696844 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 26 Feb 2012 10:41:07 +0000 Subject: - 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 --- cfrontend/Clight.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'cfrontend/Clight.v') diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index f0073a14..e4c451be 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -57,9 +57,13 @@ Inductive expr : Type := | Ebinop: binary_operation -> expr -> expr -> type -> expr (**r binary operation *) | Ecast: expr -> type -> expr (**r type cast ([(ty) e]) *) | Econdition: expr -> expr -> expr -> type -> expr (**r conditional ([e1 ? e2 : e3]) *) - | Esizeof: type -> type -> expr (**r size of a type *) | Efield: expr -> ident -> type -> expr. (**r access to a member of a struct or union *) +(** [sizeof] and [alignof] are derived forms. *) + +Definition Esizeof (ty' ty: type) : expr := Econst_int (Int.repr(sizeof ty')) ty. +Definition Ealignof (ty' ty: type) : expr := Econst_int (Int.repr(alignof ty')) ty. + (** Extract the type part of a type-annotated Clight expression. *) Definition typeof (e: expr) : type := @@ -74,7 +78,6 @@ Definition typeof (e: expr) : type := | Ebinop _ _ _ ty => ty | Ecast _ ty => ty | Econdition _ _ _ ty => ty - | Esizeof _ ty => ty | Efield _ _ ty => ty end. @@ -238,8 +241,6 @@ Inductive eval_expr: expr -> val -> Prop := | eval_Eaddrof: forall a ty loc ofs, eval_lvalue a loc ofs -> eval_expr (Eaddrof a ty) (Vptr loc ofs) - | eval_Esizeof: forall ty' ty, - eval_expr (Esizeof ty' ty) (Vint (Int.repr (sizeof ty'))) | eval_Eunop: forall op a ty v1 v, eval_expr a v1 -> sem_unary_operation op v1 (typeof a) = Some v -> -- cgit