diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
| commit | b4a08d0815342b6238d307864f0823d0f07bb691 (patch) | |
| tree | 85f48254ca79a6e2bc9d7359017a5731f98f897f /mppa_k1c/Machregsaux.ml | |
| parent | 490a6caea1a95cfdbddf7aca244fa6a1c83aa9a2 (diff) | |
| download | compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.tar.gz compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.zip | |
k1c -> kvx changes
Diffstat (limited to 'mppa_k1c/Machregsaux.ml')
| -rw-r--r-- | mppa_k1c/Machregsaux.ml | 41 |
1 files changed, 0 insertions, 41 deletions
diff --git a/mppa_k1c/Machregsaux.ml b/mppa_k1c/Machregsaux.ml deleted file mode 100644 index 76956959..00000000 --- a/mppa_k1c/Machregsaux.ml +++ /dev/null @@ -1,41 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* Xavier Leroy INRIA Paris-Rocquencourt *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. 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 - -let class_of_type = function - | AST.Tint | AST.Tlong - | AST.Tfloat | AST.Tsingle -> 0 - | AST.Tany32 | AST.Tany64 -> assert false |