diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-03 17:09:54 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-03 17:09:54 +0000 |
| commit | 362f2f36a44fa6ab4fe28264ed572d721adece70 (patch) | |
| tree | 2f1b23f88fe906ae554e963acbcde09c54b1b5fb /backend/Allocation.v | |
| parent | 089c6c6dc139a0c32f8566d028702d39d0748077 (diff) | |
| download | compcert-kvx-362f2f36a44fa6ab4fe28264ed572d721adece70.tar.gz compcert-kvx-362f2f36a44fa6ab4fe28264ed572d721adece70.zip | |
Introduce and use the platform-specific Archi module giving:
- endianness
- alignment constraints for 8-byte types
(which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Allocation.v')
| -rw-r--r-- | backend/Allocation.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 0851b77f..f830d796 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -14,6 +14,7 @@ Require Import FSets. Require FSetAVLplus. +Require Archi. Require Import Coqlib. Require Import Ordered. Require Import Errors. @@ -814,8 +815,8 @@ Definition transfer_use_def (args: list reg) (res: reg) (args': list mreg) (res' assertion (can_undef undefs e1); add_equations args args' e1. -Definition kind_first_word := if big_endian then High else Low. -Definition kind_second_word := if big_endian then Low else High. +Definition kind_first_word := if Archi.big_endian then High else Low. +Definition kind_second_word := if Archi.big_endian then Low else High. (** The core transfer function. It takes a set [e] of equations that must hold "after" and a block shape [shape] representing a matching pair |