diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:08:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:08:29 +0000 |
| commit | 73729d23ac13275c0d28d23bc1b1f6056104e5d9 (patch) | |
| tree | e3044ce75edb30377bd8c87356b7617eba5ed223 /caml/Coloringaux.ml | |
| parent | c79434827bf2bd71f857f4471f7bbf381fddd189 (diff) | |
| download | compcert-73729d23ac13275c0d28d23bc1b1f6056104e5d9.tar.gz compcert-73729d23ac13275c0d28d23bc1b1f6056104e5d9.zip | |
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
Diffstat (limited to 'caml/Coloringaux.ml')
| -rw-r--r-- | caml/Coloringaux.ml | 10 |
1 files changed, 4 insertions, 6 deletions
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 = |