From dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 15 Jun 2017 15:11:26 +0200
Subject: Extend builtin arguments with a pointer addition operator

This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.

Current status: x86 port only, the only new addressing mode handled is reg + offset.
---
 backend/XTL.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'backend/XTL.ml')

diff --git a/backend/XTL.ml b/backend/XTL.ml
index a1b7f23b..f10efeed 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -133,6 +133,7 @@ let rec type_builtin_arg a ty =
   match a with
   | BA v -> set_var_type v ty
   | BA_splitlong(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
+  | BA_addptr(a1, a2) -> type_builtin_arg a1 coq_Tptr; type_builtin_arg a2 coq_Tptr
   | _ -> ()
 
 let rec type_builtin_args al tyl =
-- 
cgit