From 5d1c52555bb166430402103afe9540cc4c296487 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Aug 2011 17:29:06 +0000 Subject: Cleaned up handling of composite conditions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgenretaddr.v | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'ia32/Asmgenretaddr.v') 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. -- cgit