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 | |
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
-rw-r--r-- | ia32/CombineOp.v | 15 | ||||
-rw-r--r-- | ia32/CombineOpproof.v | 9 |
2 files changed, 0 insertions, 24 deletions
diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v index 61f26e77..1391f556 100644 --- a/ia32/CombineOp.v +++ b/ia32/CombineOp.v @@ -68,21 +68,6 @@ Function combine_addr (addr: addressing) (args: list valnum) : option(addressing Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) := match op, args with - | Oandimm n, x :: nil => - match get x with - | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys) - | _ => None - end - | Oorimm n, x :: nil => - match get x with - | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys) - | _ => None - end - | Oxorimm n, x :: nil => - match get x with - | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys) - | _ => None - end | Olea addr, _ => match combine_addr addr args with | Some(addr', args') => Some(Olea addr', args') 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 *) |