aboutsummaryrefslogtreecommitdiffstats
path: root/arm/SelectOp.vp
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2017-05-03 11:18:32 +0200
committerGitHub <noreply@github.com>2017-05-03 11:18:32 +0200
commit7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch)
tree74500c845c99b39ba91a5507656060dea60404ea /arm/SelectOp.vp
parent25ea686abc4cce13aba92196dbeb284f727b6e0e (diff)
downloadcompcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz
compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
Diffstat (limited to 'arm/SelectOp.vp')
-rw-r--r--arm/SelectOp.vp6
1 files changed, 3 insertions, 3 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 4ea1e1a1..fc2fbe6b 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -199,7 +199,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil).
(** ** Bitwise and, or, xor *)
-Nondetfunction andimm (n1: int) (e2: expr) :=
+Nondetfunction andimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
if Int.eq n1 Int.mone then e2 else
match e2 with
@@ -343,14 +343,14 @@ Nondetfunction compimm (default: comparison -> int -> condition)
Eop (Ocmp (negate_condition c)) el
else if Int.eq_dec n2 Int.one then
Eop (Ocmp c) el
- else
+ else
Eop (Ointconst Int.zero) Enil
| Cne, Eop (Ocmp c) el =>
if Int.eq_dec n2 Int.zero then
Eop (Ocmp c) el
else if Int.eq_dec n2 Int.one then
Eop (Ocmp (negate_condition c)) el
- else
+ else
Eop (Ointconst Int.one) Enil
| _, _ =>
Eop (Ocmp (default c n2)) (e1 ::: Enil)