From e11b3b885a6d359925b86743b89698cc6757157a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 27 Mar 2015 15:28:20 +0100
Subject: Updating the PowerPC and ARM ports. PowerPC: always use full register
 names to print annotations.

---
 arm/SelectOp.vp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 6102d82d..fea99ef5 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -489,3 +489,16 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
+(** ** Arguments of annotations *)
+
+Nondetfunction annot_arg (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => AA_int n
+  | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs
+  | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs
+  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
+        AA_long (Int64.ofwords h l)
+  | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l)
+  | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs
+  | _ => AA_base e
+  end.
-- 
cgit