diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-29 09:00:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-29 09:00:26 +0000 |
commit | 2eb9e420ef5910e6b3be5735a7e38c86dcfdef36 (patch) | |
tree | 35f315de635db3488dcd3296eab3fa50c1ef8b1f /ia32/CombineOpproof.v | |
parent | 440a0bf9ab0cae2372e339cca081b01e5551e332 (diff) | |
download | compcert-2eb9e420ef5910e6b3be5735a7e38c86dcfdef36.tar.gz compcert-2eb9e420ef5910e6b3be5735a7e38c86dcfdef36.zip |
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
Diffstat (limited to 'ia32/CombineOpproof.v')
-rw-r--r-- | ia32/CombineOpproof.v | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v index c6d25093..2f1fe7bc 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 *) |