Commit ab3433fa authored by MARCHE Claude's avatar MARCHE Claude

ocaml driver: better translation of mach.int.Unsigned.zero_unsigned

parent 14645424
......@@ -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"
......
......@@ -392,6 +392,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
......@@ -423,7 +424,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