aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
Diffstat (limited to 'riscV')
-rw-r--r--riscV/Archi.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 9e561ca8..e33c3e84 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -63,11 +63,14 @@ Definition fma_invalid_mul_is_nan := false.
Definition float_of_single_preserves_sNaN := false.
+Definition float_conversion_default_nan := true.
+
Global Opaque ptr64 big_endian splitlong
default_nan_64 choose_nan_64
default_nan_32 choose_nan_32
fma_order fma_invalid_mul_is_nan
- float_of_single_preserves_sNaN.
+ float_of_single_preserves_sNaN
+ float_conversion_default_nan.
(** Whether to generate position-independent code or not *)