From 2ff53c2361773f28027ccc8332e1830686d5bbc6 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 16 Jun 2017 11:53:28 +0200
Subject: Extend builtin arguments with a pointer addition operator, continued

- Add support for PowerPC, with all addressing modes.
- Add support for ARM, with "reg + ofs" addressing mode.
- Add support for RISC-V, with the one addressing mode.
- Constprop.v: forgot to recurse in BA_addptr
- volatile4 test: more tests
---
 arm/SelectOp.vp | 1 +
 1 file changed, 1 insertion(+)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index fc2fbe6b..c361df65 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -505,5 +505,6 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
   | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) =>
        BA_loadglobal chunk id (Ptrofs.add ofs (Ptrofs.of_int ofs1))
+  | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n)
   | _ => BA e
   end.
-- 
cgit