From 362f2f36a44fa6ab4fe28264ed572d721adece70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 3 Jan 2014 17:09:54 +0000 Subject: 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 --- backend/Allocation.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backend/Allocation.v') 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 -- cgit