diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-26 10:41:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-26 10:41:07 +0000 |
commit | 2570ddd61b1c98b62c8d97fce862654535696844 (patch) | |
tree | e9a652b115045a3b2c4ade69ec3cc3fdad429b54 /cfrontend/Clight.v | |
parent | 65cc3738e7436e46f70c0508638a71fbb49c50a8 (diff) | |
download | compcert-2570ddd61b1c98b62c8d97fce862654535696844.tar.gz compcert-2570ddd61b1c98b62c8d97fce862654535696844.zip |
- 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
Diffstat (limited to 'cfrontend/Clight.v')
-rw-r--r-- | cfrontend/Clight.v | 9 |
1 files changed, 5 insertions, 4 deletions
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 -> |