From 94396a27bcfbdcb156586688de9a5a2e1bee2d4a Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 2 Nov 2021 15:43:42 +0100 Subject: [PATCH] [Ada] Create explicit ghost mirror unit for big integers gcc/ada/ * Makefile.rtl: Add unit. * libgnat/a-nbnbin__ghost.adb: Move... * libgnat/a-nbnbig.adb: ... here. Mark ghost as ignored. * libgnat/a-nbnbin__ghost.ads: Move... * libgnat/a-nbnbig.ads: ... here. Add comment for purpose of this unit. Mark ghost as ignored. * libgnat/s-widthu.adb: Use new unit. * sem_aux.adb (First_Subtype): Adapt to the case of a ghost type whose freeze node is rewritten to a null statement. --- gcc/ada/Makefile.rtl | 1 + .../{a-nbnbin__ghost.adb => a-nbnbig.adb} | 11 +++++++--- .../{a-nbnbin__ghost.ads => a-nbnbig.ads} | 20 ++++++++++++++++--- gcc/ada/libgnat/s-widthu.adb | 4 ++-- gcc/ada/sem_aux.adb | 10 +++++++++- 5 files changed, 37 insertions(+), 9 deletions(-) rename gcc/ada/libgnat/{a-nbnbin__ghost.adb => a-nbnbig.adb} (90%) rename gcc/ada/libgnat/{a-nbnbin__ghost.ads => a-nbnbig.ads} (88%) diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl index fb3f6f60a41b..282b25ce7006 100644 --- a/gcc/ada/Makefile.rtl +++ b/gcc/ada/Makefile.rtl @@ -211,6 +211,7 @@ GNATRTL_NONTASKING_OBJS= \ a-lllwti$(objext) \ a-lllzti$(objext) \ a-locale$(objext) \ + a-nbnbig$(objext) \ a-nbnbin$(objext) \ a-nbnbre$(objext) \ a-ncelfu$(objext) \ diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.adb b/gcc/ada/libgnat/a-nbnbig.adb similarity index 90% rename from gcc/ada/libgnat/a-nbnbin__ghost.adb rename to gcc/ada/libgnat/a-nbnbig.adb index 7d2208695760..d04d2a4d0197 100644 --- a/gcc/ada/libgnat/a-nbnbin__ghost.adb +++ b/gcc/ada/libgnat/a-nbnbig.adb @@ -2,7 +2,7 @@ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- -- -- -- B o d y -- -- -- @@ -33,7 +33,12 @@ -- currently does not compile instantiations of the spec with imported ghost -- generics for packages Signed_Conversions and Unsigned_Conversions. -package body Ada.Numerics.Big_Numbers.Big_Integers with +-- Ghost code in this unit is meant for analysis only, not for run-time +-- checking. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore); + +package body Ada.Numerics.Big_Numbers.Big_Integers_Ghost with SPARK_Mode => Off is @@ -73,4 +78,4 @@ is end Unsigned_Conversions; -end Ada.Numerics.Big_Numbers.Big_Integers; +end Ada.Numerics.Big_Numbers.Big_Integers_Ghost; diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbig.ads similarity index 88% rename from gcc/ada/libgnat/a-nbnbin__ghost.ads rename to gcc/ada/libgnat/a-nbnbig.ads index 3663dd7aea82..237bca19b57b 100644 --- a/gcc/ada/libgnat/a-nbnbin__ghost.ads +++ b/gcc/ada/libgnat/a-nbnbig.ads @@ -2,7 +2,7 @@ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- -- -- -- S p e c -- -- -- @@ -13,7 +13,21 @@ -- -- ------------------------------------------------------------------------------ -package Ada.Numerics.Big_Numbers.Big_Integers with +-- This unit is provided as a replacement for the standard unit +-- Ada.Numerics.Big_Numbers.Big_Integers when only proof with SPARK is +-- intended. It cannot be used for execution, as all subprograms are marked +-- imported with no definition. + +-- Contrary to Ada.Numerics.Big_Numbers.Big_Integers, this unit does not +-- depend on System or Ada.Finalization, which makes it more convenient for +-- use in run-time units. + +-- Ghost code in this unit is meant for analysis only, not for run-time +-- checking. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore); + +package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with SPARK_Mode, Ghost, Preelaborate @@ -199,4 +213,4 @@ private type Big_Integer is null record; -end Ada.Numerics.Big_Numbers.Big_Integers; +end Ada.Numerics.Big_Numbers.Big_Integers_Ghost; diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index fce8c7ad3e0c..79a0074214da 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,8 +29,8 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Numerics.Big_Numbers.Big_Integers; -use Ada.Numerics.Big_Numbers.Big_Integers; +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; function System.Width_U (Lo, Hi : Uns) return Natural is diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index dcced7e40e65..e1bcf531b719 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -336,10 +336,18 @@ package body Sem_Aux is function First_Subtype (Typ : Entity_Id) return Entity_Id is B : constant Entity_Id := Base_Type (Typ); - F : constant Node_Id := Freeze_Node (B); + F : Node_Id := Freeze_Node (B); Ent : Entity_Id; begin + -- The freeze node of a ghost type might have been rewritten in a null + -- statement by the time gigi calls First_Subtype on the corresponding + -- type. + + if Nkind (F) = N_Null_Statement then + F := Original_Node (F); + end if; + -- If the base type has no freeze node, it is a type in Standard, and -- always acts as its own first subtype, except where it is one of the -- predefined integer types. If the type is formal, it is also a first -- 2.47.2