summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-28 08:45:24 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-28 08:45:24 +0000
commit1cb7b7b8b70cb94c9bc9ef34517d95e66c4c336f (patch)
tree42d5ccdb48685298c5931c52b016e8f1ad30796d /powerpc
parentf4e106d4fc1cce484678b5cdd86ab57d7a43076a (diff)
The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Archi.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 070f7cc..058b057 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -37,6 +37,9 @@ Program Definition default_pl_32 : bool * nan_pl 24 :=
Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
false. (**r always choose first NaN *)
+Definition float_of_single_preserves_sNaN := true.
+
Global Opaque big_endian
default_pl_64 choose_binop_pl_64
- default_pl_32 choose_binop_pl_32.
+ default_pl_32 choose_binop_pl_32
+ float_of_single_preserves_sNaN.