diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-05 04:13:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-05 04:13:33 +0000 |
| commit | 0f5087bea45be49e105727d6cee4194598474fee (patch) | |
| tree | 6155d21f87a98b34ad232504d1124657ec4ed359 /powerpc/Asmgenretaddr.v | |
| parent | 1b21b6d72a4cdeb07ad646e7573983faaae47399 (diff) | |
| download | compcert-kvx-0f5087bea45be49e105727d6cee4194598474fee.tar.gz compcert-kvx-0f5087bea45be49e105727d6cee4194598474fee.zip | |
Back from Oregon commit.
powerpc/*: better compilation of some comparisons; revised asmgenproof1.
common/*: added Mem.storebytes; used to give semantics to memcpy builtin.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgenretaddr.v')
| -rw-r--r-- | powerpc/Asmgenretaddr.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index 5b1f7d53..adc15297 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -147,11 +147,18 @@ Lemma transl_cond_tail: Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed. Hint Resolve transl_cond_tail: ppcretaddr. +Lemma transl_cond_op_tail: + forall cond args r k, is_tail k (transl_cond_op cond args r k). +Proof. + unfold transl_cond_op; intros. + destruct (classify_condition cond args); IsTail. +Qed. +Hint Resolve transl_cond_op_tail: ppcretaddr. + Lemma transl_op_tail: forall op args r k, is_tail k (transl_op op args r k). Proof. unfold transl_op; intros; destruct op; IsTail. - destruct (classify_condition c args); IsTail. Qed. Hint Resolve transl_op_tail: ppcretaddr. |