[Ada] AI12-0366 Changes to Big_Integer and Big_Real

2020-06-19  Arnaud Charlet  <charlet@adacore.com>

gcc/ada/

	* libgnat/a-nbnbin.adb, libgnat/a-nbnbin.ads,
	libgnat/a-nbnbin__gmp.adb, libgnat/a-nbnbre.adb,
	libgnat/a-nbnbre.ads: Update spec according to AI12-0366.

5 files changed, 154 insertions, 167 deletions

diff --git a/gcc/ada/libgnat/a-nbnbin.adb b/gcc/ada/libgnat/a-nbnbin.adb
index fa4ddf0..9c8b733 100644
--- a/gcc/ada/libgnat/a-nbnbin.adb
+++ b/gcc/ada/libgnat/a-nbnbin.adb
@@ -77,7 +77,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "=" --
    ---------
 
-   function "=" (L, R : Big_Integer) return Boolean is
+   function "=" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return Big_EQ (Get_Bignum (L), Get_Bignum (R));
    end "=";
@@ -86,7 +86,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "<" --
    ---------
 
-   function "<" (L, R : Big_Integer) return Boolean is
+   function "<" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return Big_LT (Get_Bignum (L), Get_Bignum (R));
    end "<";
@@ -95,7 +95,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "<=" --
    ----------
 
-   function "<=" (L, R : Big_Integer) return Boolean is
+   function "<=" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return Big_LE (Get_Bignum (L), Get_Bignum (R));
    end "<=";
@@ -104,7 +104,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- ">" --
    ---------
 
-   function ">" (L, R : Big_Integer) return Boolean is
+   function ">" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return Big_GT (Get_Bignum (L), Get_Bignum (R));
    end ">";
@@ -113,7 +113,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- ">=" --
    ----------
 
-   function ">=" (L, R : Big_Integer) return Boolean is
+   function ">=" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return Big_GE (Get_Bignum (L), Get_Bignum (R));
    end ">=";
@@ -122,7 +122,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- To_Big_Integer --
    --------------------
 
-   function To_Big_Integer (Arg : Integer) return Big_Integer is
+   function To_Big_Integer (Arg : Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, To_Bignum (Long_Long_Integer (Arg)));
@@ -148,7 +148,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
       -- To_Big_Integer --
       --------------------
 
-      function To_Big_Integer (Arg : Int) return Big_Integer is
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
          Result : Big_Integer;
       begin
          Set_Bignum (Result, To_Bignum (Long_Long_Integer (Arg)));
@@ -176,7 +176,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
       -- To_Big_Integer --
       --------------------
 
-      function To_Big_Integer (Arg : Int) return Big_Integer is
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
          Result : Big_Integer;
       begin
          Set_Bignum (Result, To_Bignum (Unsigned_64 (Arg)));
@@ -201,7 +201,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    Hex_Chars : constant array (0 .. 15) of Character := "0123456789ABCDEF";
 
    function To_String
-     (Arg : Big_Integer; Width : Field := 0; Base : Number_Base := 10)
+     (Arg : Valid_Big_Integer; Width : Field := 0; Base : Number_Base := 10)
       return String
    is
       Big_Base : constant Big_Integer := To_Big_Integer (Integer (Base));
@@ -304,7 +304,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "+" --
    ---------
 
-   function "+" (L : Big_Integer) return Big_Integer is
+   function "+" (L : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, new Bignum_Data'(Get_Bignum (L).all));
@@ -315,7 +315,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "-" --
    ---------
 
-   function "-" (L : Big_Integer) return Big_Integer is
+   function "-" (L : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Neg (Get_Bignum (L)));
@@ -326,7 +326,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "abs" --
    -----------
 
-   function "abs" (L : Big_Integer) return Big_Integer is
+   function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Abs (Get_Bignum (L)));
@@ -337,7 +337,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "+" --
    ---------
 
-   function "+" (L, R : Big_Integer) return Big_Integer is
+   function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Add (Get_Bignum (L), Get_Bignum (R)));
@@ -348,7 +348,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "-" --
    ---------
 
-   function "-" (L, R : Big_Integer) return Big_Integer is
+   function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Sub (Get_Bignum (L), Get_Bignum (R)));
@@ -359,7 +359,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "*" --
    ---------
 
-   function "*" (L, R : Big_Integer) return Big_Integer is
+   function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Mul (Get_Bignum (L), Get_Bignum (R)));
@@ -370,7 +370,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "/" --
    ---------
 
-   function "/" (L, R : Big_Integer) return Big_Integer is
+   function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Div (Get_Bignum (L), Get_Bignum (R)));
@@ -381,7 +381,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "mod" --
    -----------
 
-   function "mod" (L, R : Big_Integer) return Big_Integer is
+   function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Mod (Get_Bignum (L), Get_Bignum (R)));
@@ -392,7 +392,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "rem" --
    -----------
 
-   function "rem" (L, R : Big_Integer) return Big_Integer is
+   function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Bignum (Result, Big_Rem (Get_Bignum (L), Get_Bignum (R)));
@@ -403,16 +403,9 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "**" --
    ----------
 
-   function "**" (L : Big_Integer; R : Natural) return Big_Integer is
+   function "**"
+     (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer is
    begin
-      --  Explicitly check for validity before allocating Exp so that
-      --  the call to Get_Bignum below cannot raise an exception before
-      --  we get a chance to free Exp.
-
-      if not Is_Valid (L) then
-         raise Constraint_Error with "invalid big integer";
-      end if;
-
       declare
          Exp    : Bignum := To_Bignum (Long_Long_Integer (R));
          Result : Big_Integer;
@@ -427,21 +420,23 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- Min --
    ---------
 
-   function Min (L, R : Big_Integer) return Big_Integer is
+   function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer is
      (if L < R then L else R);
 
    ---------
    -- Max --
    ---------
 
-   function Max (L, R : Big_Integer) return Big_Integer is
+   function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer is
      (if L > R then L else R);
 
    -----------------------------
    -- Greatest_Common_Divisor --
    -----------------------------
 
-   function Greatest_Common_Divisor (L, R : Big_Integer) return Big_Positive is
+   function Greatest_Common_Divisor
+     (L, R : Valid_Big_Integer) return Big_Positive
+   is
       function GCD (A, B : Big_Integer) return Big_Integer;
       --  Recursive internal version
 
diff --git a/gcc/ada/libgnat/a-nbnbin.ads b/gcc/ada/libgnat/a-nbnbin.ads
index ca77c2a..98619aa 100644
--- a/gcc/ada/libgnat/a-nbnbin.ads
+++ b/gcc/ada/libgnat/a-nbnbin.ads
@@ -23,24 +23,28 @@ private with System;
 package Ada.Numerics.Big_Numbers.Big_Integers
   with Preelaborate
 is
-   type Big_Integer is private with
-     Integer_Literal => From_String,
-     Put_Image       => Put_Image;
+   type Big_Integer is private
+     with Integer_Literal => From_String,
+          Put_Image       => Put_Image;
 
    function Is_Valid (Arg : Big_Integer) return Boolean
      with Convention => Intrinsic;
 
-   function "=" (L, R : Big_Integer) return Boolean;
+   subtype Valid_Big_Integer is Big_Integer
+     with Dynamic_Predicate => Is_Valid (Valid_Big_Integer),
+          Predicate_Failure => raise Program_Error;
 
-   function "<" (L, R : Big_Integer) return Boolean;
+   function "=" (L, R : Valid_Big_Integer) return Boolean;
 
-   function "<=" (L, R : Big_Integer) return Boolean;
+   function "<" (L, R : Valid_Big_Integer) return Boolean;
 
-   function ">" (L, R : Big_Integer) return Boolean;
+   function "<=" (L, R : Valid_Big_Integer) return Boolean;
 
-   function ">=" (L, R : Big_Integer) return Boolean;
+   function ">" (L, R : Valid_Big_Integer) return Boolean;
 
-   function To_Big_Integer (Arg : Integer) return Big_Integer;
+   function ">=" (L, R : Valid_Big_Integer) return Boolean;
+
+   function To_Big_Integer (Arg : Integer) return Valid_Big_Integer;
 
    subtype Big_Positive is Big_Integer
      with Dynamic_Predicate =>
@@ -67,7 +71,7 @@ is
       type Int is range <>;
    package Signed_Conversions is
 
-      function To_Big_Integer (Arg : Int) return Big_Integer;
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer;
 
       function From_Big_Integer (Arg : Big_Integer) return Int
         with Pre => In_Range (Arg,
@@ -81,7 +85,7 @@ is
       type Int is mod <>;
    package Unsigned_Conversions is
 
-      function To_Big_Integer (Arg : Int) return Big_Integer;
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer;
 
       function From_Big_Integer (Arg : Big_Integer) return Int
         with Pre => In_Range (Arg,
@@ -91,7 +95,7 @@ is
 
    end Unsigned_Conversions;
 
-   function To_String (Arg   : Big_Integer;
+   function To_String (Arg   : Valid_Big_Integer;
                        Width : Field := 0;
                        Base  : Number_Base := 10) return String
      with Post => To_String'Result'First = 1;
@@ -100,32 +104,32 @@ is
 
    procedure Put_Image (S : in out Sink'Class; V : Big_Integer);
 
-   function "+" (L : Big_Integer) return Big_Integer;
+   function "+" (L : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "-" (L : Big_Integer) return Big_Integer;
+   function "-" (L : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "abs" (L : Big_Integer) return Big_Integer;
+   function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "+" (L, R : Big_Integer) return Big_Integer;
+   function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "-" (L, R : Big_Integer) return Big_Integer;
+   function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "*" (L, R : Big_Integer) return Big_Integer;
+   function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "/" (L, R : Big_Integer) return Big_Integer;
+   function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "mod" (L, R : Big_Integer) return Big_Integer;
+   function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "rem" (L, R : Big_Integer) return Big_Integer;
+   function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function "**" (L : Big_Integer; R : Natural) return Big_Integer;
+   function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer;
 
-   function Min (L, R : Big_Integer) return Big_Integer;
+   function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
-   function Max (L, R : Big_Integer) return Big_Integer;
+   function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
    function Greatest_Common_Divisor
-     (L, R : Big_Integer) return Big_Positive
+     (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);
 
diff --git a/gcc/ada/libgnat/a-nbnbin__gmp.adb b/gcc/ada/libgnat/a-nbnbin__gmp.adb
index c950389..025272f 100644
--- a/gcc/ada/libgnat/a-nbnbin__gmp.adb
+++ b/gcc/ada/libgnat/a-nbnbin__gmp.adb
@@ -120,7 +120,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "=" --
    ---------
 
-   function "=" (L, R : Big_Integer) return Boolean is
+   function "=" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) = 0;
    end "=";
@@ -129,7 +129,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "<" --
    ---------
 
-   function "<" (L, R : Big_Integer) return Boolean is
+   function "<" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) < 0;
    end "<";
@@ -138,7 +138,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "<=" --
    ----------
 
-   function "<=" (L, R : Big_Integer) return Boolean is
+   function "<=" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) <= 0;
    end "<=";
@@ -147,7 +147,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- ">" --
    ---------
 
-   function ">" (L, R : Big_Integer) return Boolean is
+   function ">" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) > 0;
    end ">";
@@ -156,7 +156,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- ">=" --
    ----------
 
-   function ">=" (L, R : Big_Integer) return Boolean is
+   function ">=" (L, R : Valid_Big_Integer) return Boolean is
    begin
       return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) >= 0;
    end ">=";
@@ -165,7 +165,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- To_Big_Integer --
    --------------------
 
-   function To_Big_Integer (Arg : Integer) return Big_Integer is
+   function To_Big_Integer (Arg : Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Allocate (Result);
@@ -177,7 +177,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- To_Integer --
    ----------------
 
-   function To_Integer (Arg : Big_Integer) return Integer is
+   function To_Integer (Arg : Valid_Big_Integer) return Integer is
    begin
       return Integer (mpz_get_si (Get_Mpz (Arg)));
    end To_Integer;
@@ -192,7 +192,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
       -- To_Big_Integer --
       --------------------
 
-      function To_Big_Integer (Arg : Int) return Big_Integer is
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
          Result : Big_Integer;
       begin
          Allocate (Result);
@@ -204,7 +204,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
       -- From_Big_Integer --
       ----------------------
 
-      function From_Big_Integer (Arg : Big_Integer) return Int is
+      function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
       begin
          return Int (mpz_get_si (Get_Mpz (Arg)));
       end From_Big_Integer;
@@ -221,7 +221,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
       -- To_Big_Integer --
       --------------------
 
-      function To_Big_Integer (Arg : Int) return Big_Integer is
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
          Result : Big_Integer;
       begin
          Allocate (Result);
@@ -233,7 +233,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
       -- From_Big_Integer --
       ----------------------
 
-      function From_Big_Integer (Arg : Big_Integer) return Int is
+      function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
       begin
          return Int (mpz_get_ui (Get_Mpz (Arg)));
       end From_Big_Integer;
@@ -245,7 +245,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    ---------------
 
    function To_String
-     (Arg : Big_Integer; Width : Field := 0; Base : Number_Base := 10)
+     (Arg : Valid_Big_Integer; Width : Field := 0; Base : Number_Base := 10)
       return String
    is
       function mpz_get_str
@@ -330,7 +330,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- From_String --
    -----------------
 
-   function From_String (Arg : String) return Big_Integer is
+   function From_String (Arg : String) return Valid_Big_Integer is
       function mpz_set_str
         (this : access mpz_t;
          str  : System.Address;
@@ -417,7 +417,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "+" --
    ---------
 
-   function "+" (L : Big_Integer) return Big_Integer is
+   function "+" (L : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Set_Mpz (Result, new mpz_t);
@@ -429,7 +429,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "-" --
    ---------
 
-   function "-" (L : Big_Integer) return Big_Integer is
+   function "-" (L : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Allocate (Result);
@@ -441,7 +441,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "abs" --
    -----------
 
-   function "abs" (L : Big_Integer) return Big_Integer is
+   function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer is
       procedure mpz_abs (ROP : access mpz_t;  OP : access constant mpz_t);
       pragma Import (C, mpz_abs, "__gmpz_abs");
 
@@ -456,7 +456,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "+" --
    ---------
 
-   function "+" (L, R : Big_Integer) return Big_Integer is
+   function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       procedure mpz_add
         (ROP : access mpz_t;  OP1, OP2 : access constant mpz_t);
       pragma Import (C, mpz_add, "__gmpz_add");
@@ -473,7 +473,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "-" --
    ---------
 
-   function "-" (L, R : Big_Integer) return Big_Integer is
+   function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       Result : Big_Integer;
    begin
       Allocate (Result);
@@ -485,7 +485,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "*" --
    ---------
 
-   function "*" (L, R : Big_Integer) return Big_Integer is
+   function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       procedure mpz_mul
         (ROP : access mpz_t;  OP1, OP2 : access constant mpz_t);
       pragma Import (C, mpz_mul, "__gmpz_mul");
@@ -502,7 +502,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "/" --
    ---------
 
-   function "/" (L, R : Big_Integer) return Big_Integer is
+   function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       procedure mpz_tdiv_q (Q : access mpz_t;  N, D : access constant mpz_t);
       pragma Import (C, mpz_tdiv_q, "__gmpz_tdiv_q");
    begin
@@ -523,7 +523,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "mod" --
    -----------
 
-   function "mod" (L, R : Big_Integer) return Big_Integer is
+   function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       procedure mpz_mod (R : access mpz_t;  N, D : access constant mpz_t);
       pragma Import (C, mpz_mod, "__gmpz_mod");
       --  result is always non-negative
@@ -605,7 +605,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "rem" --
    -----------
 
-   function "rem" (L, R : Big_Integer) return Big_Integer is
+   function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
       procedure mpz_tdiv_r (R : access mpz_t;  N, D : access constant mpz_t);
       pragma Import (C, mpz_tdiv_r, "__gmpz_tdiv_r");
       --   R will have the same sign as N.
@@ -632,7 +632,9 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- "**" --
    ----------
 
-   function "**" (L : Big_Integer; R : Natural) return Big_Integer is
+   function "**"
+     (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer
+   is
       procedure mpz_pow_ui (ROP : access mpz_t;
                             BASE : access constant mpz_t;
                             EXP : unsigned_long);
@@ -650,21 +652,23 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is
    -- Min --
    ---------
 
-   function Min (L, R : Big_Integer) return Big_Integer is
+   function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer is
      (if L < R then L else R);
 
    ---------
    -- Max --
    ---------
 
-   function Max (L, R : Big_Integer) return Big_Integer is
+   function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer is
      (if L > R then L else R);
 
    -----------------------------
    -- Greatest_Common_Divisor --
    -----------------------------
 
-   function Greatest_Common_Divisor (L, R : Big_Integer) return Big_Positive is
+   function Greatest_Common_Divisor
+     (L, R : Valid_Big_Integer) return Big_Positive
+   is
       procedure mpz_gcd
         (ROP : access mpz_t;  Op1, Op2 : access constant mpz_t);
       pragma Import (C, mpz_gcd, "__gmpz_gcd");
diff --git a/gcc/ada/libgnat/a-nbnbre.adb b/gcc/ada/libgnat/a-nbnbre.adb
index 11459ca..1f075df 100644
--- a/gcc/ada/libgnat/a-nbnbre.adb
+++ b/gcc/ada/libgnat/a-nbnbre.adb
@@ -54,7 +54,7 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "/" --
    ---------
 
-   function "/" (Num, Den : Big_Integer) return Big_Real is
+   function "/" (Num, Den : Valid_Big_Integer) return Valid_Big_Real is
       Result : Big_Real;
    begin
       if Den = To_Big_Integer (0) then
@@ -71,49 +71,47 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- Numerator --
    ---------------
 
-   function Numerator (Arg : Big_Real) return Big_Integer is
-     (if Is_Valid (Arg.Num) then Arg.Num
-      else raise Constraint_Error with "invalid big real");
+   function Numerator (Arg : Valid_Big_Real) return Valid_Big_Integer is
+     (Arg.Num);
 
    -----------------
    -- Denominator --
    -----------------
 
-   function Denominator (Arg : Big_Real) return Big_Positive is
-     (if Is_Valid (Arg.Den) then Arg.Den
-      else raise Constraint_Error with "invalid big real");
+   function Denominator (Arg : Valid_Big_Real) return Big_Positive is
+     (Arg.Den);
 
    ---------
    -- "=" --
    ---------
 
-   function "=" (L, R : Big_Real) return Boolean is
+   function "=" (L, R : Valid_Big_Real) return Boolean is
      (abs L.Num = abs R.Num and then L.Den = R.Den);
 
    ---------
    -- "<" --
    ---------
 
-   function "<" (L, R : Big_Real) return Boolean is
+   function "<" (L, R : Valid_Big_Real) return Boolean is
      (abs L.Num * R.Den < abs R.Num * L.Den);
 
    ----------
    -- "<=" --
    ----------
 
-   function "<=" (L, R : Big_Real) return Boolean is (not (R < L));
+   function "<=" (L, R : Valid_Big_Real) return Boolean is (not (R < L));
 
    ---------
    -- ">" --
    ---------
 
-   function ">" (L, R : Big_Real) return Boolean is (R < L);
+   function ">" (L, R : Valid_Big_Real) return Boolean is (R < L);
 
    ----------
    -- ">=" --
    ----------
 
-   function ">=" (L, R : Big_Real) return Boolean is (not (L < R));
+   function ">=" (L, R : Valid_Big_Real) return Boolean is (not (L < R));
 
    -----------------------
    -- Float_Conversions --
@@ -125,7 +123,7 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
       -- To_Big_Real --
       -----------------
 
-      function To_Big_Real (Arg : Num) return Big_Real is
+      function To_Big_Real (Arg : Num) return Valid_Big_Real is
       begin
          return From_String (Arg'Image);
       end To_Big_Real;
@@ -151,7 +149,7 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
       -- To_Big_Real --
       -----------------
 
-      function To_Big_Real (Arg : Num) return Big_Real is
+      function To_Big_Real (Arg : Num) return Valid_Big_Real is
       begin
          return From_String (Arg'Image);
       end To_Big_Real;
@@ -172,8 +170,10 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    ---------------
 
    function To_String
-     (Arg : Big_Real; Fore : Field := 2; Aft : Field := 3; Exp : Field := 0)
-      return String
+     (Arg  : Valid_Big_Real;
+      Fore : Field := 2;
+      Aft  : Field := 3;
+      Exp  : Field := 0) return String
    is
       Zero : constant Big_Integer := To_Big_Integer (0);
       Ten  : constant Big_Integer := To_Big_Integer (10);
@@ -379,7 +379,7 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- From_Quotient_String --
    --------------------------
 
-   function From_Quotient_String (Arg : String) return Big_Real is
+   function From_Quotient_String (Arg : String) return Valid_Big_Real is
       Index : Natural := 0;
    begin
       for J in Arg'First + 1 .. Arg'Last - 1 loop
@@ -413,13 +413,9 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "+" --
    ---------
 
-   function "+" (L : Big_Real) return Big_Real is
+   function "+" (L : Valid_Big_Real) return Valid_Big_Real is
       Result : Big_Real;
    begin
-      if not Is_Valid (L) then
-         raise Constraint_Error with "invalid big real";
-      end if;
-
       Result.Num := L.Num;
       Result.Den := L.Den;
       return Result;
@@ -429,29 +425,23 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "-" --
    ---------
 
-   function "-" (L : Big_Real) return Big_Real is
-     (if Is_Valid (L) then (Num => -L.Num, Den => L.Den)
-      else raise Constraint_Error with "invalid big real");
+   function "-" (L : Valid_Big_Real) return Valid_Big_Real is
+     (Num => -L.Num, Den => L.Den);
 
    -----------
    -- "abs" --
    -----------
 
-   function "abs" (L : Big_Real) return Big_Real is
-     (if Is_Valid (L) then (Num => abs L.Num, Den => L.Den)
-      else raise Constraint_Error with "invalid big real");
+   function "abs" (L : Valid_Big_Real) return Valid_Big_Real is
+     (Num => abs L.Num, Den => L.Den);
 
    ---------
    -- "+" --
    ---------
 
-   function "+" (L, R : Big_Real) return Big_Real is
+   function "+" (L, R : Valid_Big_Real) return Valid_Big_Real is
       Result : Big_Real;
    begin
-      if not Is_Valid (L) or not Is_Valid (R) then
-         raise Constraint_Error with "invalid big real";
-      end if;
-
       Result.Num := L.Num * R.Den + R.Num * L.Den;
       Result.Den := L.Den * R.Den;
       Normalize (Result);
@@ -462,13 +452,9 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "-" --
    ---------
 
-   function "-" (L, R : Big_Real) return Big_Real is
+   function "-" (L, R : Valid_Big_Real) return Valid_Big_Real is
       Result : Big_Real;
    begin
-      if not Is_Valid (L) or not Is_Valid (R) then
-         raise Constraint_Error with "invalid big real";
-      end if;
-
       Result.Num := L.Num * R.Den - R.Num * L.Den;
       Result.Den := L.Den * R.Den;
       Normalize (Result);
@@ -479,13 +465,9 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "*" --
    ---------
 
-   function "*" (L, R : Big_Real) return Big_Real is
+   function "*" (L, R : Valid_Big_Real) return Valid_Big_Real is
       Result : Big_Real;
    begin
-      if not Is_Valid (L) or not Is_Valid (R) then
-         raise Constraint_Error with "invalid big real";
-      end if;
-
       Result.Num := L.Num * R.Num;
       Result.Den := L.Den * R.Den;
       Normalize (Result);
@@ -496,13 +478,9 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "/" --
    ---------
 
-   function "/" (L, R : Big_Real) return Big_Real is
+   function "/" (L, R : Valid_Big_Real) return Valid_Big_Real is
       Result : Big_Real;
    begin
-      if not Is_Valid (L) or not Is_Valid (R) then
-         raise Constraint_Error with "invalid big real";
-      end if;
-
       Result.Num := L.Num * R.Den;
       Result.Den := L.Den * R.Num;
       Normalize (Result);
@@ -513,13 +491,9 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- "**" --
    ----------
 
-   function "**" (L : Big_Real; R : Integer) return Big_Real is
+   function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real is
       Result : Big_Real;
    begin
-      if not Is_Valid (L) then
-         raise Constraint_Error with "invalid big real";
-      end if;
-
       if R = 0 then
          Result.Num := To_Big_Integer (1);
          Result.Den := To_Big_Integer (1);
@@ -542,13 +516,15 @@ package body Ada.Numerics.Big_Numbers.Big_Reals is
    -- Min --
    ---------
 
-   function Min (L, R : Big_Real) return Big_Real is (if L < R then L else R);
+   function Min (L, R : Valid_Big_Real) return Valid_Big_Real is
+     (if L < R then L else R);
 
    ---------
    -- Max --
    ---------
 
-   function Max (L, R : Big_Real) return Big_Real is (if L > R then L else R);
+   function Max (L, R : Valid_Big_Real) return Valid_Big_Real is
+     (if L > R then L else R);
 
    ---------------
    -- Normalize --
diff --git a/gcc/ada/libgnat/a-nbnbre.ads b/gcc/ada/libgnat/a-nbnbre.ads
index 44958b4..2915db0 100644
--- a/gcc/ada/libgnat/a-nbnbre.ads
+++ b/gcc/ada/libgnat/a-nbnbre.ads
@@ -29,36 +29,44 @@ is
    function Is_Valid (Arg : Big_Real) return Boolean
      with Convention => Intrinsic;
 
-   function "/" (Num, Den : Big_Integers.Big_Integer) return Big_Real;
---   with Pre => (if Big_Integers."=" (Den, Big_Integers.To_Big_Integer (0))
---                then raise Constraint_Error);
+   subtype Valid_Big_Real is Big_Real
+     with Dynamic_Predicate => Is_Valid (Valid_Big_Real),
+          Predicate_Failure => raise Program_Error;
 
-   function Numerator (Arg : Big_Real) return Big_Integers.Big_Integer;
+   function "/"
+     (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real;
+--   with Pre => (Big_Integers."/=" (Den, Big_Integers.To_Big_Integer (0))
+--                or else Constraint_Error);
 
-   function Denominator (Arg : Big_Real) return Big_Integers.Big_Positive
+   function Numerator
+     (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer;
+
+   function Denominator (Arg : Valid_Big_Real) return Big_Integers.Big_Positive
      with Post =>
-       (Arg = To_Real (0)) or else
-       (Big_Integers."="
-         (Big_Integers.Greatest_Common_Divisor
-           (Numerator (Arg), Denominator'Result),
-          Big_Integers.To_Big_Integer (1)));
+       (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)));
 
    function To_Big_Real
      (Arg : Big_Integers.Big_Integer)
-     return Big_Real is (Arg / Big_Integers.To_Big_Integer (1));
+     return Valid_Big_Real is (Arg / Big_Integers.To_Big_Integer (1));
 
-   function To_Real (Arg : Integer) return Big_Real is
+   function To_Real (Arg : Integer) return Valid_Big_Real is
      (Big_Integers.To_Big_Integer (Arg) / Big_Integers.To_Big_Integer (1));
 
-   function "=" (L, R : Big_Real) return Boolean;
+   function "=" (L, R : Valid_Big_Real) return Boolean;
 
-   function "<" (L, R : Big_Real) return Boolean;
+   function "<" (L, R : Valid_Big_Real) return Boolean;
 
-   function "<=" (L, R : Big_Real) return Boolean;
+   function "<=" (L, R : Valid_Big_Real) return Boolean;
 
-   function ">" (L, R : Big_Real) return Boolean;
+   function ">" (L, R : Valid_Big_Real) return Boolean;
 
-   function ">=" (L, R : Big_Real) return Boolean;
+   function ">=" (L, R : Valid_Big_Real) return Boolean;
 
    function In_Range (Arg, Low, High : Big_Real) return Boolean is
      (Low <= Arg and then Arg <= High);
@@ -67,7 +75,7 @@ is
       type Num is digits <>;
    package Float_Conversions is
 
-      function To_Big_Real (Arg : Num) return Big_Real;
+      function To_Big_Real (Arg : Num) return Valid_Big_Real;
 
       function From_Big_Real (Arg : Big_Real) return Num
         with Pre => In_Range (Arg,
@@ -81,7 +89,7 @@ is
       type Num is delta <>;
    package Fixed_Conversions is
 
-      function To_Big_Real (Arg : Num) return Big_Real;
+      function To_Big_Real (Arg : Num) return Valid_Big_Real;
 
       function From_Big_Real (Arg : Big_Real) return Num
         with Pre => In_Range (Arg,
@@ -91,7 +99,7 @@ is
 
    end Fixed_Conversions;
 
-   function To_String (Arg  : Big_Real;
+   function To_String (Arg  : Valid_Big_Real;
                        Fore : Field := 2;
                        Aft  : Field := 3;
                        Exp  : Field := 0) return String
@@ -103,29 +111,29 @@ is
      (Big_Integers.To_String (Numerator (Arg)) & " / "
       & Big_Integers.To_String (Denominator (Arg)));
 
-   function From_Quotient_String (Arg : String) return Big_Real;
+   function From_Quotient_String (Arg : String) return Valid_Big_Real;
 
    procedure Put_Image (S : in out Sink'Class; V : Big_Real);
 
-   function "+" (L : Big_Real) return Big_Real;
+   function "+" (L : Valid_Big_Real) return Valid_Big_Real;
 
-   function "-" (L : Big_Real) return Big_Real;
+   function "-" (L : Valid_Big_Real) return Valid_Big_Real;
 
-   function "abs" (L : Big_Real) return Big_Real;
+   function "abs" (L : Valid_Big_Real) return Valid_Big_Real;
 
-   function "+" (L, R : Big_Real) return Big_Real;
+   function "+" (L, R : Valid_Big_Real) return Valid_Big_Real;
 
-   function "-" (L, R : Big_Real) return Big_Real;
+   function "-" (L, R : Valid_Big_Real) return Valid_Big_Real;
 
-   function "*" (L, R : Big_Real) return Big_Real;
+   function "*" (L, R : Valid_Big_Real) return Valid_Big_Real;
 
-   function "/" (L, R : Big_Real) return Big_Real;
+   function "/" (L, R : Valid_Big_Real) return Valid_Big_Real;
 
-   function "**" (L : Big_Real; R : Integer) return Big_Real;
+   function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real;
 
-   function Min (L, R : Big_Real) return Big_Real;
+   function Min (L, R : Valid_Big_Real) return Valid_Big_Real;
 
-   function Max (L, R : Big_Real) return Big_Real;
+   function Max (L, R : Valid_Big_Real) return Valid_Big_Real;
 
 private