diff options
author | Yannick Moy <moy@adacore.com> | 2022-02-10 10:31:05 +0100 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-12 12:38:38 +0000 |
commit | bbb4320baea245dc5abab35aba7d6225bc9f70fe (patch) | |
tree | ff6f2d5506578f996900b7a6a4bbc683b0001ef5 /gcc/ada/libgnat | |
parent | 6655b152ebbf97e66888dc003414f6bb62a7edab (diff) | |
download | gcc-bbb4320baea245dc5abab35aba7d6225bc9f70fe.zip gcc-bbb4320baea245dc5abab35aba7d6225bc9f70fe.tar.gz gcc-bbb4320baea245dc5abab35aba7d6225bc9f70fe.tar.bz2 |
[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.
Diffstat (limited to 'gcc/ada/libgnat')
-rw-r--r-- | gcc/ada/libgnat/s-aridou.ads | 14 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-exponn.ads | 10 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-expont.ads | 10 | ||||
-rw-r--r-- | 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 815865f..29e13a5 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 2c95f60..5c6eeac 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 7ca43ab..99de227 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 2c583b3..b6ae541 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; |