From: Yannick Moy Date: Thu, 10 Feb 2022 09:31:05 +0000 (+0100) Subject: [Ada] Remove use of use-clauses in loaded runtime units X-Git-Tag: basepoints/gcc-14~6848 X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=bbb4320baea245dc5abab35aba7d6225bc9f70fe;p=thirdparty%2Fgcc.git [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 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;