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) | |
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 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 *) |