aboutsummaryrefslogtreecommitdiffstats
path: root/arm/SelectOp.vp
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2016-10-27 16:26:08 +0200
committerGitHub <noreply@github.com>2016-10-27 16:26:08 +0200
commit9922feea537ced718a3822dd50eabc87da060338 (patch)
tree6f67bb6707ef59e50d6bb81c61b2ed0b3c6097ab /arm/SelectOp.vp
parentf2d6637c7d4a11f961ff289e64f70bf4de93d0aa (diff)
parentd50773e537ec6729f9152b545c6f938ab19eb7b8 (diff)
downloadcompcert-9922feea537ced718a3822dd50eabc87da060338.tar.gz
compcert-9922feea537ced718a3822dd50eabc87da060338.zip
Merge pull request #145 from AbsInt/64
Support for 64-bit target processors + support for x86 in 64-bit mode
Diffstat (limited to 'arm/SelectOp.vp')
-rw-r--r--arm/SelectOp.vp10
1 files changed, 5 insertions, 5 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index aec737ad..80a5d753 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -48,10 +48,10 @@ Open Local Scope cminorsel_scope.
(** ** Constants **)
-Definition addrsymbol (id: ident) (ofs: int) :=
+Definition addrsymbol (id: ident) (ofs: ptrofs) :=
Eop (Oaddrsymbol id ofs) Enil.
-Definition addrstack (ofs: int) :=
+Definition addrstack (ofs: ptrofs) :=
Eop (Oaddrstack ofs) Enil.
(** ** Integer logical negation *)
@@ -72,8 +72,8 @@ Nondetfunction addimm (n: int) (e: expr) :=
if Int.eq n Int.zero then e else
match e with
| Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil
- | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil
- | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil
+ | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
+ | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
| Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
| _ => Eop (Oaddimm n) (e ::: Enil)
end.
@@ -501,6 +501,6 @@ Nondetfunction builtin_arg (e: expr) :=
| Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
| Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
| Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) =>
- BA_loadglobal chunk id (Int.add ofs ofs1)
+ BA_loadglobal chunk id (Ptrofs.add ofs (Ptrofs.of_int ofs1))
| _ => BA e
end.