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.
Tested on x86_64-pc-linux-gnu, committed on trunk
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
--- 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
--- 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
--- 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
--- 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;
