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 --- backend/Constprop.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend') diff --git a/backend/Constprop.v b/backend/Constprop.v index 151f8418..d8211ffe 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -98,6 +98,8 @@ Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) := | BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo) | hi', lo' => BA_splitlong hi' lo' end + | BA_addptr a1 a2 => + BA_addptr (builtin_arg_reduction ae a1) (builtin_arg_reduction ae a2) | _ => a end. -- cgit