summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
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.