From 5ad466befa609df178f04886484ee38b1a9c44ed Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 23 Apr 2015 14:49:30 +0200
Subject: Take asm clobbers into account for determining callee-save registers
 used.

---
 extraction/extraction.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'extraction')

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 1db52ef3..4c400036 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -22,6 +22,7 @@ Require Inlining.
 Require ValueDomain.
 Require Tailcall.
 Require Allocation.
+Require Bounds.
 Require Ctypes.
 Require Csyntax.
 Require Ctyping.
@@ -76,6 +77,9 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc".
 (* Linearize *)
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
+(* Bounds *)
+Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber".
+
 (* SimplExpr *)
 Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident".
 Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
-- 
cgit