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

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

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:bbb4320baea245dc5abab35aba7d6225bc9f70fe

commit r13-359-gbbb4320baea245dc5abab35aba7d6225bc9f70fe
Author: Yannick Moy <moy@adacore.com>
Date:   Thu Feb 10 10:31:05 2022 +0100

    [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:
---
 gcc/ada/libgnat/s-aridou.ads | 14 ++++++++++----
 gcc/ada/libgnat/s-exponn.ads | 10 ++++++----
 gcc/ada/libgnat/s-expont.ads | 10 ++++++----
 gcc/ada/libgnat/s-widthu.ads | 10 ++++++++--
 4 files changed, 30 insertions(+), 14 deletions(-)

diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads
index 815865f53ca..29e13a5979a 100644
--- 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 2c95f608f9e..5c6eeac03ee 100644
--- 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 7ca43ab1723..99de227bd6f 100644
--- 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 2c583b31c6c..b6ae5417293 100644
--- 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;