aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGuillaume Melquiond2019-12-27 09:04:39 +0400
committerGuillaume Melquiond2019-12-27 18:53:38 +0400
commit00c0b652311b8c6b26c7e21b17db4ab12a35f286 (patch)
treef0f8effc012a2d43d8ffe6b723b8de7b6e11201d /kernel
parent4e176a7ee4660d505321ca55c5ce70a6c3d50d3b (diff)
Add critical-bugs entry, tests-suite file, and code comment.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/uint63_31.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index ddb6ba656e..445166f6af 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -132,6 +132,7 @@ let mulc x y =
(* add the outer products *)
let lr = Int64.add (Int64.mul lx ly) lr in
let hr = Int64.add (Int64.mul hx hy) hr in
+ (* hr fits on 64 bits, since the final result fits on 126 bits *)
(* now x * y = hr * 2^62 + lr and lr < 2^63 *)
let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in
let hr = Int64.shift_right_logical hr 1 in