From 2ff53c2361773f28027ccc8332e1830686d5bbc6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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 --- riscV/SelectOp.vp | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'riscV/SelectOp.vp') diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index b38b7b4d..bb8af2ed 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -442,5 +442,9 @@ Nondetfunction builtin_arg (e: expr) := BA_long (Int64.ofwords h l) | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | Eop (Oaddimm n) (e1:::Enil) => + if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) + | Eop (Oaddlimm n) (e1:::Enil) => + if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. -- cgit