[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.

diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index fb3f6f6..282b25c 100644 (file)
--- 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 7d22086..d04d2a4 100644 (file)
--- 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 3663dd7..237bca1 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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