- 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, 6 insertions, 0 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b3c3f6b..f589fab 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -787,6 +787,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       end
   | RV, Esizeof ty' ty =>
       topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0)
+  | RV, Ealignof ty' ty =>
+      topred (Rred (Eval (Vint (Int.repr (alignof ty'))) ty) m E0)
   | RV, Eassign l1 r2 ty =>
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
@@ -1363,6 +1365,8 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext_ok; eauto.
 (* sizeof *)
   apply topred_ok; auto. split. apply red_sizeof. exists w; constructor.
+(* alignof *)
+  apply topred_ok; auto. split. apply red_alignof. exists w; constructor.
 (* assign *)
   destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. 
   destruct (is_val a2) as [[v2 ty2] | ]_eqn. 
@@ -1494,6 +1498,8 @@ Proof.
   inv H0. rewrite H; auto.
 (* sizeof *)
   inv H. auto.
+(* alignof *)
+  inv H. auto.
 (* assign *)
   rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto.
 (* assignop *)