(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) open Registers open Locations open RTL open RTLtyping open InterfGraph val graph_coloring: coq_function -> graph -> regenv -> Regset.t -> (reg -> loc) val reserved_registers: Machregs.mreg list ref