diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 3 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_emul.h | 4 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_native.h | 9 |
3 files changed, 8 insertions, 8 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index c21aeecb16..ca1308696c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1711,7 +1711,8 @@ value coq_interprete print_instr("CHECKLDSHIFTEXP"); CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); Swap_accu_sp; - Int_of_uint63(accu); + Uint63_to_int_min(accu, Val_int(2 * FLOAT_EXP_SHIFT)); + accu = Int_val(accu); Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT)); Next; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index e09803ae2d..143a6d098c 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -169,5 +169,5 @@ DECLARE_UNOP(of_float) DECLARE_UNOP(of_int) #define Uint63_of_int(x) CALL_UNOP(of_int, x) -DECLARE_UNOP(to_int_saturate) -#define Int_of_uint63(x) CALL_PREDICATE(accu, to_int_saturate, x) +DECLARE_BINOP(to_int_min) +#define Uint63_to_int_min(n, m) CALL_BINOP(to_int_min, n, m) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 0ab374194e..5be7587091 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -155,10 +155,9 @@ value coq_uint63_to_float_byte(value x) { #define Uint63_of_int(x) (accu = (x)) -#define Int_of_uint63(x) do{ \ - uint64_t int_of_uint63__ = uint63_of_value(x); \ - if ((int_of_uint63__ & 0xFFFFFFFF80000000L) == 0) \ - accu = (int)int_of_uint63__; \ +#define Uint63_to_int_min(n, m) do { \ + if (uint63_lt((n),(m))) \ + accu = (n); \ else \ - accu = 0x7FFFFFFF; \ + accu = (m); \ }while(0) |