diff options
| author | Guillaume Bertholon | 2018-08-03 17:38:48 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:27 +0100 |
| commit | dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 (patch) | |
| tree | ad80b6386f39dda5666308658ef7d9fa79c4cd20 /kernel | |
| parent | 55d32c9f3a91058f69f34c17c17701d0dc81874d (diff) | |
Put axioms on ldshiftexp and frshiftexp
Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas.
The shift value has been increased to 2 * emax + prec because in ldexp
we want to be able to transform the smallest denormalized to the biggest
float value in one call.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_values.h | 2 | ||||
| -rw-r--r-- | kernel/float64.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 14f3f152bf..fa51b2d31f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -45,6 +45,6 @@ #define coq_tag_Some 1 #define coq_None Val_int(0) -#define FLOAT_EXP_SHIFT (1022 + 52) +#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ #endif /* _COQ_VALUES_ */ diff --git a/kernel/float64.ml b/kernel/float64.ml index 0b22e07e82..a625c0f551 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -51,7 +51,7 @@ let normfr_mantissa f = if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec) else Uint63.zero -let eshift = 1022 + 52 (* minimum negative exponent + binary precision *) +let eshift = 2101 (* 2*emax + prec *) (* When calling frexp on a nan or an infinity, the returned value inside the exponent is undefined. |