So far, only one light runtime units was using the standard unit for
big integers. A special ghost mirror had been created for the reduced
runtimes. In order to use more liberally big integers for proof of the
runtime, rename this ghost mirror into Big_Integers_Ghost at the same
level in the hierarchy of units as Big_Integers.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
--- 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
--- 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
--- 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
--- 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
--- 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
