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

1 files changed, 10 insertions, 3 deletions

diff --git a/arm/Nan.v b/arm/Archi.v
index e2bddf6..e693541 100644
--- a/arm/Nan.v
+++ b/arm/Archi.v
@@ -14,11 +14,16 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(** Architecture-dependent parameters for ARM *)
+
+Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
-Require Import Floats.
-Require Import ZArith.
-Require Import Integers.
+
+Definition big_endian := false.
+
+Notation align_int64 := 8%Z (only parsing).
+Notation align_float64 := 8%Z (only parsing).
 
 Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH).
 
@@ -27,3 +32,5 @@ Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 5
       In all other cases, choose first NaN *)
   (Pos.testbit (proj1_sig pl1) 51 &&
    negb (Pos.testbit (proj1_sig pl2) 51))%bool.
+
+Global Opaque big_endian default_pl choose_binop_pl.