diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-14 09:58:40 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-14 09:58:40 +0000 |
commit | 5955f24c579250be7701a8f351be4b627d670b81 (patch) | |
tree | 64279e0c703253d32e65bd7e95c3527fad54d342 /backend/Coloring.v | |
parent | 0180f46a9f47f9611974d77844fd860ffa49d679 (diff) | |
download | compcert-5955f24c579250be7701a8f351be4b627d670b81.tar.gz compcert-5955f24c579250be7701a8f351be4b627d670b81.zip |
Add preference for annot_val builtin
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1674 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Coloring.v')
-rw-r--r-- | backend/Coloring.v | 9 |
1 files changed, 8 insertions, 1 deletions
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 |