diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-05 17:29:06 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-05 17:29:06 +0000 |
| commit | 5d1c52555bb166430402103afe9540cc4c296487 (patch) | |
| tree | 2a23a9acb86dca39f1b04c46f3913ec35e30be79 /ia32/Asmgenretaddr.v | |
| parent | a80483e9f8ec927bfd1f32a117c56c8167cecc4f (diff) | |
| download | compcert-5d1c52555bb166430402103afe9540cc4c296487.tar.gz compcert-5d1c52555bb166430402103afe9540cc4c296487.zip | |
Cleaned up handling of composite conditions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgenretaddr.v')
| -rw-r--r-- | ia32/Asmgenretaddr.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v index 674a73e1..e0787d72 100644 --- a/ia32/Asmgenretaddr.v +++ b/ia32/Asmgenretaddr.v @@ -173,8 +173,24 @@ Proof. unfold storeind; intros. destruct ty; IsTail. destruct (preg_of src); IsTail. Qed. +Lemma mk_setcc_tail: + forall cond rd k, is_tail k (mk_setcc cond rd k). +Proof. + unfold mk_setcc; intros. destruct cond. + IsTail. + destruct (ireg_eq rd EDX); IsTail. + destruct (ireg_eq rd EDX); IsTail. +Qed. + +Lemma mk_jcc_tail: + forall cond lbl k, is_tail k (mk_jcc cond lbl k). +Proof. + unfold mk_jcc; intros. destruct cond; IsTail. +Qed. + Hint Resolve mk_mov_tail mk_shift_tail mk_div_tail mk_mod_tail mk_shrximm_tail - mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail : ppcretaddr. + mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail + mk_setcc_tail mk_jcc_tail : ppcretaddr. Lemma transl_cond_tail: forall cond args k c, transl_cond cond args k = OK c -> is_tail k c. |