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 --- arm/Machregs.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Machregs.v') diff --git a/arm/Machregs.v b/arm/Machregs.v index e97df790..ba3bda7c 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -197,8 +197,8 @@ Global Opaque two_address_op. Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := match ef with - | EF_vload _ => OK_addrany :: nil - | EF_vstore _ => OK_addrany :: OK_default :: nil + | EF_vload _ => OK_addressing :: nil + | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil | EF_annot txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs -- cgit