diff options
Diffstat (limited to 'ia32/Machregsaux.ml')
| -rw-r--r-- | ia32/Machregsaux.ml | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml deleted file mode 100644 index 473e0602..00000000 --- a/ia32/Machregsaux.ml +++ /dev/null @@ -1,33 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(** Auxiliary functions on machine registers *) - -open Camlcoq -open Machregs - -let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 - -let _ = - List.iter - (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) - Machregs.register_names - -let is_scratch_register r = false - -let name_of_register r = - try Some (Hashtbl.find register_names r) with Not_found -> None - -let register_by_name s = - Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) - -let can_reserve_register r = Conventions1.is_callee_save r |