diff options
Diffstat (limited to 'gcc/ada/libgnat/s-arit64.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-arit64.ads | 96 |
1 files changed, 5 insertions, 91 deletions
diff --git a/gcc/ada/libgnat/s-arit64.ads b/gcc/ada/libgnat/s-arit64.ads index 2ddd15c..6e12789 100644 --- a/gcc/ada/libgnat/s-arit64.ads +++ b/gcc/ada/libgnat/s-arit64.ads @@ -36,49 +36,14 @@ pragma Restrictions (No_Elaboration_Code); -- Allow direct call from gigi generated code --- Preconditions in this unit are meant for analysis only, not for run-time --- checking, so that the expected exceptions are raised. This is enforced --- by setting the corresponding assertion policy to Ignore. Postconditions --- and contract cases should not be executed at runtime as well, in order --- not to slow down the execution of these functions. - -pragma Assertion_Policy (Pre => Ignore, - Post => Ignore, - Contract_Cases => Ignore, - Ghost => Ignore); - -with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; with Interfaces; package System.Arith_64 with Pure, SPARK_Mode is - use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer; - use type Interfaces.Integer_64; - subtype Int64 is Interfaces.Integer_64; - subtype Big_Integer is - Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer - with Ghost; - - package Signed_Conversion is new - Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Signed_Conversions - (Int => Int64); - - function Big (Arg : Int64) return Big_Integer is - (Signed_Conversion.To_Big_Integer (Arg)) - with Ghost; - - function In_Int64_Range (Arg : Big_Integer) return Boolean is - (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range - (Arg, Big (Int64'First), Big (Int64'Last))) - with Ghost; - - function Add_With_Ovflo_Check64 (X, Y : Int64) return Int64 - with - Pre => In_Int64_Range (Big (X) + Big (Y)), - Post => Add_With_Ovflo_Check64'Result = X + Y; + function Add_With_Ovflo_Check64 (X, Y : Int64) return Int64; -- Raises Constraint_Error if sum of operands overflows 64 bits, -- otherwise returns the 64-bit signed integer sum. -- @@ -93,10 +58,7 @@ is -- the exception *Constraint_Error* is raised; otherwise the result is -- correct. - function Subtract_With_Ovflo_Check64 (X, Y : Int64) return Int64 - with - Pre => In_Int64_Range (Big (X) - Big (Y)), - Post => Subtract_With_Ovflo_Check64'Result = X - Y; + function Subtract_With_Ovflo_Check64 (X, Y : Int64) return Int64; -- Raises Constraint_Error if difference of operands overflows 64 -- bits, otherwise returns the 64-bit signed integer difference. -- @@ -105,10 +67,7 @@ is -- a sign of the result is compared with the sign of ``X`` to check for -- overflow. - function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64 - with - Pre => In_Int64_Range (Big (X) * Big (Y)), - Post => Multiply_With_Ovflo_Check64'Result = X * Y; + function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64; pragma Export (C, Multiply_With_Ovflo_Check64, "__gnat_mulv64"); -- Raises Constraint_Error if product of operands overflows 64 -- bits, otherwise returns the 64-bit signed integer product. @@ -119,40 +78,10 @@ is -- signed value is returned. Overflow check is performed by looking at -- higher digits. - function Same_Sign (X, Y : Big_Integer) return Boolean is - (X = Big (Int64'(0)) - or else Y = Big (Int64'(0)) - or else (X < Big (Int64'(0))) = (Y < Big (Int64'(0)))) - with Ghost; - - function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer with - Ghost, - Pre => Y /= 0 and then Q = X / Y and then R = X rem Y, - Post => Round_Quotient'Result = - (if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then - (if Same_Sign (X, Y) then Q + Big (Int64'(1)) - else Q - Big (Int64'(1))) - else - Q); - procedure Scaled_Divide64 (X, Y, Z : Int64; Q, R : out Int64; - Round : Boolean) - with - Pre => Z /= 0 - and then In_Int64_Range - (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z), - Big (X) * Big (Y) / Big (Z), - Big (X) * Big (Y) rem Big (Z)) - else Big (X) * Big (Y) / Big (Z)), - Post => Big (R) = Big (X) * Big (Y) rem Big (Z) - and then - (if Round then - Big (Q) = Round_Quotient (Big (X) * Big (Y), Big (Z), - Big (X) * Big (Y) / Big (Z), Big (R)) - else - Big (Q) = Big (X) * Big (Y) / Big (Z)); + Round : Boolean); -- Performs the division of (``X`` * ``Y``) / ``Z``, storing the quotient -- in ``Q`` and the remainder in ``R``. -- @@ -189,22 +118,7 @@ is procedure Double_Divide64 (X, Y, Z : Int64; Q, R : out Int64; - Round : Boolean) - with - Pre => Y /= 0 - and then Z /= 0 - and then In_Int64_Range - (if Round then Round_Quotient (Big (X), Big (Y) * Big (Z), - Big (X) / (Big (Y) * Big (Z)), - Big (X) rem (Big (Y) * Big (Z))) - else Big (X) / (Big (Y) * Big (Z))), - Post => Big (R) = Big (X) rem (Big (Y) * Big (Z)) - and then - (if Round then - Big (Q) = Round_Quotient (Big (X), Big (Y) * Big (Z), - Big (X) / (Big (Y) * Big (Z)), Big (R)) - else - Big (Q) = Big (X) / (Big (Y) * Big (Z))); + Round : Boolean); -- Performs the division ``X`` / (``Y`` * ``Z``), storing the quotient in -- ``Q`` and the remainder in ``R``. Constraint_Error is raised if ``Y`` or -- ``Z`` is zero, or if the quotient does not fit in 64-bits. |