aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Machregsaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Machregsaux.ml')
-rw-r--r--aarch64/Machregsaux.ml19
1 files changed, 0 insertions, 19 deletions
diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml
index f13a9ff5..41db3bd4 100644
--- a/aarch64/Machregsaux.ml
+++ b/aarch64/Machregsaux.ml
@@ -12,28 +12,9 @@
(** 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 s =
s = "X16" || s = "x16" || s = "X30" || s = "x30"
-
-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
-
let class_of_type = function
| AST.Tint | AST.Tlong -> 0
| AST.Tfloat | AST.Tsingle -> 1