From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Feb 2013 16:24:13 +0000 Subject: Pointers one past git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgen.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'arm/Asmgen.v') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index b78dfb66..05e7010e 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -57,9 +57,9 @@ Definition is_immed_mem_float (x: int) : bool := Fixpoint decompose_int_rec (N: nat) (n p: int) : list int := match N with | Datatypes.O => - if Int.eq_dec n Int.zero then nil else n :: nil + if Int.eq n Int.zero then nil else n :: nil | Datatypes.S M => - if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then + if Int.eq (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then decompose_int_rec M n (Int.add p (Int.repr 2)) else let m := Int.shl (Int.repr 255) p in @@ -86,14 +86,14 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) Definition loadimm (r: ireg) (n: int) (k: code) := let d1 := decompose_int n in let d2 := decompose_int (Int.not n) in - if le_dec (List.length d1) (List.length d2) + if NPeano.leb (List.length d1) (List.length d2) then iterate_op (Pmov r) (Porr r r) d1 k else iterate_op (Pmvn r) (Pbic r r) d2 k. Definition addimm (r1 r2: ireg) (n: int) (k: code) := let d1 := decompose_int n in let d2 := decompose_int (Int.neg n) in - if le_dec (List.length d1) (List.length d2) + if NPeano.leb (List.length d1) (List.length d2) then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k. -- cgit