From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/Coloringaux.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'caml/Coloringaux.ml') diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml index f4f4bcd3..a7c8db5c 100644 --- a/caml/Coloringaux.ml +++ b/caml/Coloringaux.ml @@ -266,15 +266,13 @@ let class_of_type = function Tint -> 0 | Tfloat -> 1 let num_register_classes = 2 let caller_save_registers = [| - [| R3; R4; R5; R6; R7; R8; R9; R10 |]; - [| F1; F2; F3; F4; F5; F6; F7; F8; F9; F10 |] + array_of_coqlist Conventions.int_caller_save_regs; + array_of_coqlist Conventions.float_caller_save_regs |] let callee_save_registers = [| - [| R13; R14; R15; R16; R17; R18; R19; R20; R21; R22; - R23; R24; R25; R26; R27; R28; R29; R30; R31 |]; - [| F14; F15; F16; F17; F18; F19; F20; F21; F22; - F23; F24; F25; F26; F27; F28; F29; F30; F31 |] + array_of_coqlist Conventions.int_callee_save_regs; + array_of_coqlist Conventions.float_callee_save_regs |] let num_available_registers = -- cgit