diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-10-27 16:26:08 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-10-27 16:26:08 +0200 |
commit | 9922feea537ced718a3822dd50eabc87da060338 (patch) | |
tree | 6f67bb6707ef59e50d6bb81c61b2ed0b3c6097ab /arm/SelectOp.vp | |
parent | f2d6637c7d4a11f961ff289e64f70bf4de93d0aa (diff) | |
parent | d50773e537ec6729f9152b545c6f938ab19eb7b8 (diff) | |
download | compcert-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.vp | 10 |
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. |