summaryrefslogtreecommitdiff
path: root/ia32/CombineOp.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-05-29 09:00:26 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-05-29 09:00:26 +0000
commit2eb9e420ef5910e6b3be5735a7e38c86dcfdef36 (patch)
tree35f315de635db3488dcd3296eab3fa50c1ef8b1f /ia32/CombineOp.v
parent440a0bf9ab0cae2372e339cca081b01e5551e332 (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/CombineOp.v')
-rw-r--r--ia32/CombineOp.v15
1 files changed, 0 insertions, 15 deletions
diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
index 61f26e7..1391f55 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')