a-lllwti$(objext) \
a-lllzti$(objext) \
a-locale$(objext) \
+ a-nbnbig$(objext) \
a-nbnbin$(objext) \
a-nbnbre$(objext) \
a-ncelfu$(objext) \
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
--- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS --
+-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST --
-- --
-- B o d y --
-- --
-- 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
end Unsigned_Conversions;
-end Ada.Numerics.Big_Numbers.Big_Integers;
+end Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
--- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS --
+-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST --
-- --
-- S p e c --
-- --
-- --
------------------------------------------------------------------------------
-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
type Big_Integer is null record;
-end Ada.Numerics.Big_Numbers.Big_Integers;
+end Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-- --
------------------------------------------------------------------------------
-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
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