From 9e76f90bc5255d6ec933d705bf99baf3ca80d5d5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Jul 2012 09:00:24 +0000 Subject: Updated ARM port. CSE.v: removed commented-out stuff. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/CombineOp.v | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'arm/CombineOp.v') diff --git a/arm/CombineOp.v b/arm/CombineOp.v index be9824bc..fd347c1b 100644 --- a/arm/CombineOp.v +++ b/arm/CombineOp.v @@ -74,13 +74,16 @@ Function combine_cond (cond: condition) (args: list valnum) : option(condition * | _, _ => None end. +(* Problem: on ARM, not all load/store instructions accept the Aindexed2 + and Aindexed2shift addressing modes. For the time being, + avoid producing them. *) + Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) := match addr, args with | Aindexed n, x::nil => match get x with - | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys) - | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None - | Some(Op (Oaddshift s) ys) => if Int.eq_dec n Int.zero then Some(Aindexed2shift s, ys) else None + | Some(Op (Oaddimm m) ys) => + Some(Aindexed (Int.add m n), ys) | _ => None end | _, _ => None -- cgit