From 2eb9e420ef5910e6b3be5735a7e38c86dcfdef36 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 May 2012 09:00:26 +0000 Subject: Removed Oandimm, etc, cases, because of 2-address constraints... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1904 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/CombineOpproof.v | 9 --------- 1 file changed, 9 deletions(-) (limited to 'ia32/CombineOpproof.v') diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v index c6d2509..2f1fe7b 100644 --- a/ia32/CombineOpproof.v +++ b/ia32/CombineOpproof.v @@ -112,15 +112,6 @@ Theorem combine_op_sound: eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m. Proof. intros. functional inversion H; subst. -(* andimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.and_assoc. auto. -(* orimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.or_assoc. auto. -(* xorimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.xor_assoc. auto. (* lea *) simpl. eapply combine_addr_sound; eauto. (* cmp *) -- cgit v1.2.3