[Ada] Remove use of use-clauses in loaded runtime units

The spec of runtime units that may be loaded by the compiler should not
contain use-clauses, for visibility to be correctly handled.  Remove
use-clauses that were introduced for the ghost big integers unit as part
of the proof of runtime units.

gcc/ada/

	* libgnat/s-aridou.ads: Remove use-clause, add renames and
	subtypes.
	* libgnat/s-exponn.ads: Same.
	* libgnat/s-expont.ads: Same.
	* libgnat/s-widthu.ads: Same.

diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads
index 815865f..29e13a5 100644 (file)
--- a/gcc/ada/libgnat/s-aridou.ads
+++ b/gcc/ada/libgnat/s-aridou.ads
@@ -34,7 +34,6 @@
 --  or intermediate results are longer than the result type.
 
 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
 generic
 
@@ -67,20 +66,27 @@ is
                             Contract_Cases => Ignore,
                             Ghost          => Ignore);
 
-   package Signed_Conversion is new Signed_Conversions (Int => Double_Int);
+   package BI_Ghost renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+   subtype Big_Integer is BI_Ghost.Big_Integer with Ghost;
+   subtype Big_Natural is BI_Ghost.Big_Natural with Ghost;
+   use type BI_Ghost.Big_Integer;
+
+   package Signed_Conversion is
+     new BI_Ghost.Signed_Conversions (Int => Double_Int);
 
    function Big (Arg : Double_Int) return Big_Integer is
      (Signed_Conversion.To_Big_Integer (Arg))
    with Ghost;
 
-   package Unsigned_Conversion is new Unsigned_Conversions (Int => Double_Uns);
+   package Unsigned_Conversion is
+     new BI_Ghost.Unsigned_Conversions (Int => Double_Uns);
 
    function Big (Arg : Double_Uns) return Big_Integer is
      (Unsigned_Conversion.To_Big_Integer (Arg))
    with Ghost;
 
    function In_Double_Int_Range (Arg : Big_Integer) return Boolean is
-     (In_Range (Arg, Big (Double_Int'First), Big (Double_Int'Last)))
+     (BI_Ghost.In_Range (Arg, Big (Double_Int'First), Big (Double_Int'Last)))
    with Ghost;
 
    function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int

diff --git a/gcc/ada/libgnat/s-exponn.ads b/gcc/ada/libgnat/s-exponn.ads
index 2c95f60..5c6eeac 100644 (file)
--- a/gcc/ada/libgnat/s-exponn.ads
+++ b/gcc/ada/libgnat/s-exponn.ads
@@ -32,7 +32,6 @@
 --  Signed integer exponentiation (checks off)
 
 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
 generic
 
@@ -41,7 +40,6 @@ generic
 package System.Exponn
   with Pure, SPARK_Mode
 is
-
    --  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
@@ -53,14 +51,18 @@ is
                             Contract_Cases => Ignore,
                             Ghost          => Ignore);
 
-   package Signed_Conversion is new Signed_Conversions (Int => Int);
+   package BI_Ghost renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+   subtype Big_Integer is BI_Ghost.Big_Integer with Ghost;
+   use type BI_Ghost.Big_Integer;
+
+   package Signed_Conversion is new BI_Ghost.Signed_Conversions (Int => Int);
 
    function Big (Arg : Int) return Big_Integer is
      (Signed_Conversion.To_Big_Integer (Arg))
    with Ghost;
 
    function In_Int_Range (Arg : Big_Integer) return Boolean is
-     (In_Range (Arg, Big (Int'First), Big (Int'Last)))
+     (BI_Ghost.In_Range (Arg, Big (Int'First), Big (Int'Last)))
    with Ghost;
 
    function Expon (Left : Int; Right : Natural) return Int

diff --git a/gcc/ada/libgnat/s-expont.ads b/gcc/ada/libgnat/s-expont.ads
index 7ca43ab..99de227 100644 (file)
--- a/gcc/ada/libgnat/s-expont.ads
+++ b/gcc/ada/libgnat/s-expont.ads
@@ -32,7 +32,6 @@
 --  Signed integer exponentiation (checks on)
 
 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
 generic
 
@@ -41,7 +40,6 @@ generic
 package System.Expont
   with Pure, SPARK_Mode
 is
-
    --  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
@@ -53,14 +51,18 @@ is
                             Contract_Cases => Ignore,
                             Ghost          => Ignore);
 
-   package Signed_Conversion is new Signed_Conversions (Int => Int);
+   package BI_Ghost renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+   subtype Big_Integer is BI_Ghost.Big_Integer with Ghost;
+   use type BI_Ghost.Big_Integer;
+
+   package Signed_Conversion is new BI_Ghost.Signed_Conversions (Int => Int);
 
    function Big (Arg : Int) return Big_Integer is
      (Signed_Conversion.To_Big_Integer (Arg))
    with Ghost;
 
    function In_Int_Range (Arg : Big_Integer) return Boolean is
-     (In_Range (Arg, Big (Int'First), Big (Int'Last)))
+     (BI_Ghost.In_Range (Arg, Big (Int'First), Big (Int'Last)))
    with Ghost;
 
    function Expon (Left : Int; Right : Natural) return Int

diff --git a/gcc/ada/libgnat/s-widthu.ads b/gcc/ada/libgnat/s-widthu.ads
index 2c583b3..b6ae541 100644 (file)
--- a/gcc/ada/libgnat/s-widthu.ads
+++ b/gcc/ada/libgnat/s-widthu.ads
@@ -45,7 +45,6 @@ pragma Assertion_Policy (Pre                => Ignore,
 --  type. The arguments Lo, Hi are the bounds of the type.
 
 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
 generic
 
@@ -54,7 +53,14 @@ generic
 package System.Width_U
   with Pure
 is
-   package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
+   package BI_Ghost renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+   subtype Big_Integer is BI_Ghost.Big_Integer with Ghost;
+   subtype Big_Natural is BI_Ghost.Big_Natural with Ghost;
+   subtype Big_Positive is BI_Ghost.Big_Positive with Ghost;
+   use type BI_Ghost.Big_Integer;
+
+   package Unsigned_Conversion is
+     new BI_Ghost.Unsigned_Conversions (Int => Uns);
 
    function Big (Arg : Uns) return Big_Integer renames
      Unsigned_Conversion.To_Big_Integer;