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/Cexec.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'cfrontend/Cexec.v') 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 *) -- cgit v1.2.3