From 028aaefc44b8ed8bafd8b8896fedb53f6e68df3c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 5 Aug 2016 14:05:34 +0200 Subject: Implement support for big endian arm targets. Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418 --- arm/Archi.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'arm/Archi.v') diff --git a/arm/Archi.v b/arm/Archi.v index 6b282022..fedc55f5 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -20,7 +20,7 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. -Definition big_endian := false. +Parameter big_endian: bool. Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). @@ -45,8 +45,7 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := false. -Global Opaque big_endian - default_pl_64 choose_binop_pl_64 +Global Opaque default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. -- cgit