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

1 files changed, 21 insertions, 0 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index ce90ebee..ae5a1017 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -1338,3 +1338,24 @@ Proof.
 Qed.
 
 End EVAL_INJECT.
+
+(** * Handling of builtin arguments *)
+
+Definition builtin_arg_ok_1
+       (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
+  match c, ba with
+  | OK_all, _ => true
+  | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true
+  | OK_addrstack, BA_addrstack _ => true
+  | OK_addressing, BA_addrstack _ => true
+  | OK_addressing, BA_addptr (BA _) (BA_int _) => true
+  | OK_addressing, BA_addptr (BA _) (BA_long _) => true
+  | _, _ => false
+  end.
+
+Definition builtin_arg_ok
+       (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
+  match ba with
+  | (BA _ | BA_splitlong (BA _) (BA _)) => true
+  | _ => builtin_arg_ok_1 ba c
+  end.