diff options
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/Makefile.rtl | 1 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-nbnbig.adb (renamed from gcc/ada/libgnat/a-nbnbin__ghost.adb) | 11 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-nbnbig.ads (renamed from gcc/ada/libgnat/a-nbnbin__ghost.ads) | 20 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-widthu.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_aux.adb | 10 |
5 files changed, 37 insertions, 9 deletions
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl index fb3f6f6..282b25c 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 index 7d22086..d04d2a4 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 index 3663dd7..237bca1 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 fce8c7a..79a0074 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 dcced7e..e1bcf53 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 |