From faa1d7fbfd7c9d5aa333d9b353a6118e105c4428 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sat, 25 Apr 2020 16:52:33 +0200 Subject: Remove the `can_reserve_register` function. The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`. --- aarch64/Machregsaux.ml | 2 -- arm/Machregsaux.ml | 4 ---- arm/Machregsaux.mli | 1 - cfrontend/CPragmas.ml | 2 +- powerpc/Machregsaux.ml | 4 ---- powerpc/Machregsaux.mli | 1 - riscV/Machregsaux.ml | 2 -- riscV/Machregsaux.mli | 1 - x86/Machregsaux.ml | 2 -- x86/Machregsaux.mli | 1 - 10 files changed, 1 insertion(+), 19 deletions(-) diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index 39008965..7d233041 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -31,5 +31,3 @@ let name_of_register r = 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 diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml index 21425851..7d278613 100644 --- a/arm/Machregsaux.ml +++ b/arm/Machregsaux.ml @@ -29,7 +29,3 @@ let name_of_register r = let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) - -let can_reserve_register r = - List.mem r Conventions1.int_callee_save_regs - || List.mem r Conventions1.float_callee_save_regs diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli index 9404568d..884100bb 100644 --- a/arm/Machregsaux.mli +++ b/arm/Machregsaux.mli @@ -15,4 +15,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool -val can_reserve_register: Machregs.mreg -> bool diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index ce2cfcf0..92cf4cec 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -56,7 +56,7 @@ let process_reserve_register_pragma name = | None -> C2C.error "unknown register in `reserve_register' pragma" | Some r -> - if Machregsaux.can_reserve_register r then + if Conventions1.is_callee_save r then reserved_registers := r :: !reserved_registers else C2C.error "cannot reserve this register (not a callee-save)" diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index 711eb623..40c993fd 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -29,7 +29,3 @@ let name_of_register r = let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) - -let can_reserve_register r = - List.mem r Conventions1.int_callee_save_regs - || List.mem r Conventions1.float_callee_save_regs diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index 9404568d..884100bb 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -15,4 +15,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool -val can_reserve_register: Machregs.mreg -> bool diff --git a/riscV/Machregsaux.ml b/riscV/Machregsaux.ml index 82d3803e..a273bb51 100644 --- a/riscV/Machregsaux.ml +++ b/riscV/Machregsaux.ml @@ -29,5 +29,3 @@ let name_of_register r = 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 diff --git a/riscV/Machregsaux.mli b/riscV/Machregsaux.mli index 9404568d..884100bb 100644 --- a/riscV/Machregsaux.mli +++ b/riscV/Machregsaux.mli @@ -15,4 +15,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool -val can_reserve_register: Machregs.mreg -> bool diff --git a/x86/Machregsaux.ml b/x86/Machregsaux.ml index 82d3803e..a273bb51 100644 --- a/x86/Machregsaux.ml +++ b/x86/Machregsaux.ml @@ -29,5 +29,3 @@ let name_of_register r = 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 diff --git a/x86/Machregsaux.mli b/x86/Machregsaux.mli index 9404568d..884100bb 100644 --- a/x86/Machregsaux.mli +++ b/x86/Machregsaux.mli @@ -15,4 +15,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool -val can_reserve_register: Machregs.mreg -> bool -- cgit