From 5955f24c579250be7701a8f351be4b627d670b81 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 14 Jun 2011 09:58:40 +0000
Subject: Add preference for annot_val builtin

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1674 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Coloring.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'backend/Coloring.v')

diff --git a/backend/Coloring.v b/backend/Coloring.v
index 6d34e2cc..a23bf55f 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -139,6 +139,13 @@ Fixpoint add_prefs_call
   | _, _ => g
   end.
 
+Definition add_prefs_builtin (ef: external_function)
+                            (args: list reg) (res: reg) (g: graph) : graph :=
+  match ef, args with
+  | EF_annot_val txt targ, arg1 :: _ => add_pref arg1 res g
+  | _, _ => g
+  end.
+
 Definition add_interf_entry
     (params: list reg) (live: Regset.t) (g: graph): graph :=
   List.fold_left (fun g r => add_interf_op r live g) params g.
@@ -184,7 +191,7 @@ Definition add_edges_instr
       add_prefs_call args largs
         (add_interf_call ros largs g)
   | Ibuiltin ef args res s =>
-      add_interf_op res live g
+      add_prefs_builtin ef args res (add_interf_op res live g)
   | Ireturn (Some r) =>
       add_pref_mreg r (loc_result sig) g
   | _ => g
-- 
cgit