[Ada] Add global contracts to Ada.Numerics.Big_Numbers libraries
authorJoffrey Huguet <huguet@adacore.com>
Tue, 26 May 2020 16:06:58 +0000 (18:06 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 10 Jul 2020 09:16:18 +0000 (05:16 -0400)
gcc/ada/

* libgnat/a-nbnbin.ads, libgnat/a-nbnbre.ads: Add global
contract (Global => null) to all functions.

gcc/ada/libgnat/a-nbnbin.ads
gcc/ada/libgnat/a-nbnbre.ads

index 74232f9cbe815dbb1c15fe11690aab603c6eae4b..5cf7960db10c816aad46f213d3cb10774bc707b0 100644 (file)
@@ -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
 
index 2915db025b62cca44a3f8bbdaa76e5e6bba1f54d..2d4ff63f64fb854a9900787f9ee051e0e5bc8fa5 100644 (file)
@@ -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