From 25af525c300abc790ef35bf2d8fb083a570b840a Mon Sep 17 00:00:00 2001 From: Joffrey Huguet Date: Tue, 26 May 2020 18:06:58 +0200 Subject: [PATCH] [Ada] Add global contracts to Ada.Numerics.Big_Numbers libraries gcc/ada/ * libgnat/a-nbnbin.ads, libgnat/a-nbnbre.ads: Add global contract (Global => null) to all functions. --- gcc/ada/libgnat/a-nbnbin.ads | 107 ++++++++++++++++++++++------------- gcc/ada/libgnat/a-nbnbre.ads | 104 ++++++++++++++++++++++------------ 2 files changed, 135 insertions(+), 76 deletions(-) diff --git a/gcc/ada/libgnat/a-nbnbin.ads b/gcc/ada/libgnat/a-nbnbin.ads index 74232f9cbe8..5cf7960db10 100644 --- a/gcc/ada/libgnat/a-nbnbin.ads +++ b/gcc/ada/libgnat/a-nbnbin.ads @@ -28,23 +28,26 @@ is Put_Image => Put_Image; function Is_Valid (Arg : Big_Integer) return Boolean - with Convention => Intrinsic; + with + Convention => Intrinsic, + Global => null; subtype Valid_Big_Integer is Big_Integer with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), Predicate_Failure => raise Program_Error; - function "=" (L, R : Valid_Big_Integer) return Boolean; + function "=" (L, R : Valid_Big_Integer) return Boolean with Global => null; - function "<" (L, R : Valid_Big_Integer) return Boolean; + function "<" (L, R : Valid_Big_Integer) return Boolean with Global => null; - function "<=" (L, R : Valid_Big_Integer) return Boolean; + function "<=" (L, R : Valid_Big_Integer) return Boolean with Global => null; - function ">" (L, R : Valid_Big_Integer) return Boolean; + function ">" (L, R : Valid_Big_Integer) return Boolean with Global => null; - function ">=" (L, R : Valid_Big_Integer) return Boolean; + function ">=" (L, R : Valid_Big_Integer) return Boolean with Global => null; - function To_Big_Integer (Arg : Integer) return Valid_Big_Integer; + function To_Big_Integer (Arg : Integer) return Valid_Big_Integer + with Global => null; subtype Big_Positive is Big_Integer with Dynamic_Predicate => @@ -60,79 +63,105 @@ is function In_Range (Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean - is (Low <= Arg and Arg <= High); + is (Low <= Arg and Arg <= High) + with + Global => null; function To_Integer (Arg : Valid_Big_Integer) return Integer - with Pre => In_Range (Arg, - Low => To_Big_Integer (Integer'First), - High => To_Big_Integer (Integer'Last)) - or else (raise Constraint_Error); + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Integer'First), + High => To_Big_Integer (Integer'Last)) + or else (raise Constraint_Error), + Global => null; generic type Int is range <>; package Signed_Conversions is - function To_Big_Integer (Arg : Int) return Valid_Big_Integer; + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with Global => null; function From_Big_Integer (Arg : Valid_Big_Integer) return Int - with Pre => In_Range (Arg, - Low => To_Big_Integer (Int'First), - High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error); - + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; end Signed_Conversions; generic type Int is mod <>; package Unsigned_Conversions is - function To_Big_Integer (Arg : Int) return Valid_Big_Integer; + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with Global => null; function From_Big_Integer (Arg : Valid_Big_Integer) return Int - with Pre => In_Range (Arg, - Low => To_Big_Integer (Int'First), - High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error); + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; end Unsigned_Conversions; function To_String (Arg : Valid_Big_Integer; Width : Field := 0; Base : Number_Base := 10) return String - with Post => To_String'Result'First = 1; + with + Post => To_String'Result'First = 1, + Global => null; - function From_String (Arg : String) return Big_Integer; + function From_String (Arg : String) return Big_Integer + with Global => null; procedure Put_Image (S : in out Sink'Class; V : Big_Integer); - function "+" (L : Valid_Big_Integer) return Valid_Big_Integer; + function "+" (L : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "-" (L : Valid_Big_Integer) return Valid_Big_Integer; + function "-" (L : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer; + function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer; + function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer + with Global => null; - function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; - function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer; + function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer + with Global => null; function Greatest_Common_Divisor (L, R : Valid_Big_Integer) return Big_Positive - with Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0)) - or else (raise Constraint_Error); + with + Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0)) + or else (raise Constraint_Error), + Global => null; private diff --git a/gcc/ada/libgnat/a-nbnbre.ads b/gcc/ada/libgnat/a-nbnbre.ads index 2915db025b6..2d4ff63f64f 100644 --- a/gcc/ada/libgnat/a-nbnbre.ads +++ b/gcc/ada/libgnat/a-nbnbre.ads @@ -27,61 +27,73 @@ is Put_Image => Put_Image; function Is_Valid (Arg : Big_Real) return Boolean - with Convention => Intrinsic; + with + Convention => Intrinsic, + Global => null; subtype Valid_Big_Real is Big_Real with Dynamic_Predicate => Is_Valid (Valid_Big_Real), Predicate_Failure => raise Program_Error; function "/" - (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real; + (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real + with Global => null; -- with Pre => (Big_Integers."/=" (Den, Big_Integers.To_Big_Integer (0)) -- or else Constraint_Error); function Numerator - (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer; + (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer + with Global => null; function Denominator (Arg : Valid_Big_Real) return Big_Integers.Big_Positive - with Post => + with + Post => (if Arg = To_Real (0) then Big_Integers."=" (Denominator'Result, Big_Integers.To_Big_Integer (1)) else Big_Integers."=" (Big_Integers.Greatest_Common_Divisor (Numerator (Arg), Denominator'Result), - Big_Integers.To_Big_Integer (1))); + Big_Integers.To_Big_Integer (1))), + Global => null; function To_Big_Real (Arg : Big_Integers.Big_Integer) - return Valid_Big_Real is (Arg / Big_Integers.To_Big_Integer (1)); + return Valid_Big_Real is (Arg / Big_Integers.To_Big_Integer (1)) + with Global => null; function To_Real (Arg : Integer) return Valid_Big_Real is - (Big_Integers.To_Big_Integer (Arg) / Big_Integers.To_Big_Integer (1)); + (Big_Integers.To_Big_Integer (Arg) / Big_Integers.To_Big_Integer (1)) + with Global => null; - function "=" (L, R : Valid_Big_Real) return Boolean; + function "=" (L, R : Valid_Big_Real) return Boolean with Global => null; - function "<" (L, R : Valid_Big_Real) return Boolean; + function "<" (L, R : Valid_Big_Real) return Boolean with Global => null; - function "<=" (L, R : Valid_Big_Real) return Boolean; + function "<=" (L, R : Valid_Big_Real) return Boolean with Global => null; - function ">" (L, R : Valid_Big_Real) return Boolean; + function ">" (L, R : Valid_Big_Real) return Boolean with Global => null; - function ">=" (L, R : Valid_Big_Real) return Boolean; + function ">=" (L, R : Valid_Big_Real) return Boolean with Global => null; function In_Range (Arg, Low, High : Big_Real) return Boolean is - (Low <= Arg and then Arg <= High); + (Low <= Arg and then Arg <= High) + with Global => null; generic type Num is digits <>; package Float_Conversions is - function To_Big_Real (Arg : Num) return Valid_Big_Real; + function To_Big_Real (Arg : Num) return Valid_Big_Real + with Global => null; function From_Big_Real (Arg : Big_Real) return Num - with Pre => In_Range (Arg, - Low => To_Big_Real (Num'First), - High => To_Big_Real (Num'Last)) - or else (raise Constraint_Error); + with + Pre => In_Range (Arg, + Low => To_Big_Real (Num'First), + High => To_Big_Real (Num'Last)) + or else (raise Constraint_Error), + Global => null; end Float_Conversions; @@ -89,13 +101,16 @@ is type Num is delta <>; package Fixed_Conversions is - function To_Big_Real (Arg : Num) return Valid_Big_Real; + function To_Big_Real (Arg : Num) return Valid_Big_Real + with Global => null; function From_Big_Real (Arg : Big_Real) return Num - with Pre => In_Range (Arg, - Low => To_Big_Real (Num'First), - High => To_Big_Real (Num'Last)) - or else (raise Constraint_Error); + with + Pre => In_Range (Arg, + Low => To_Big_Real (Num'First), + High => To_Big_Real (Num'Last)) + or else (raise Constraint_Error), + Global => null; end Fixed_Conversions; @@ -103,37 +118,52 @@ is Fore : Field := 2; Aft : Field := 3; Exp : Field := 0) return String - with Post => To_String'Result'First = 1; + with + Post => To_String'Result'First = 1, + Global => null; - function From_String (Arg : String) return Big_Real; + function From_String (Arg : String) return Big_Real + with Global => null; function To_Quotient_String (Arg : Big_Real) return String is (Big_Integers.To_String (Numerator (Arg)) & " / " - & Big_Integers.To_String (Denominator (Arg))); + & Big_Integers.To_String (Denominator (Arg))) + with Global => null; - function From_Quotient_String (Arg : String) return Valid_Big_Real; + function From_Quotient_String (Arg : String) return Valid_Big_Real + with Global => null; procedure Put_Image (S : in out Sink'Class; V : Big_Real); - function "+" (L : Valid_Big_Real) return Valid_Big_Real; + function "+" (L : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "-" (L : Valid_Big_Real) return Valid_Big_Real; + function "-" (L : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "abs" (L : Valid_Big_Real) return Valid_Big_Real; + function "abs" (L : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "+" (L, R : Valid_Big_Real) return Valid_Big_Real; + function "+" (L, R : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "-" (L, R : Valid_Big_Real) return Valid_Big_Real; + function "-" (L, R : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "*" (L, R : Valid_Big_Real) return Valid_Big_Real; + function "*" (L, R : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "/" (L, R : Valid_Big_Real) return Valid_Big_Real; + function "/" (L, R : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real; + function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real + with Global => null; - function Min (L, R : Valid_Big_Real) return Valid_Big_Real; + function Min (L, R : Valid_Big_Real) return Valid_Big_Real + with Global => null; - function Max (L, R : Valid_Big_Real) return Valid_Big_Real; + function Max (L, R : Valid_Big_Real) return Valid_Big_Real + with Global => null; private -- 2.30.2