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/Cexec.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/Cexec.v')
-rw-r--r-- | cfrontend/Cexec.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b3c3f6b8..f589fab3 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 *) |