aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/SelectOp.vp
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/SelectOp.vp')
-rw-r--r--powerpc/SelectOp.vp15
1 files changed, 15 insertions, 0 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 70b1feb6..618643b8 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -523,3 +523,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
| _ => (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 (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs
+ | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs
+ | _ => AA_base e
+ end.