Commit 77a7ca18 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'claude'

parents 503ddd14 ab3433fa
......@@ -31,6 +31,7 @@ module mach.int.UInt32
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax constant zero_unsigned "0L"
syntax type uint32 "Int64.t"
syntax val (+) "Int64.add"
......
......@@ -393,6 +393,7 @@ module N
raises { TooManyDigits -> true }
= let lx = x.digits.length in
let ly = y.digits.length in
(* TODO: predict carry to enlarge with 1 more cell if carry may occur *)
if Int31.(<) lx ly then enlarge x ly;
add_aux_in_place x y.digits
......@@ -424,7 +425,8 @@ module N
let add (x y:t) : t
ensures { value result = value x + value y }
raises { TooManyDigits -> true }
= let lx = x.digits.length in
= (* TODO: just copy x or y and call add_in_place, and throw away add_array *)
let lx = x.digits.length in
let ly = y.digits.length in
if Int31.(>=) lx ly then
{ digits = add_array x.digits y.digits }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment