public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-5090] [Ada] Create explicit ghost mirror unit for big integers
@ 2021-11-10 8:58 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-11-10 8:58 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:94396a27bcfbdcb156586688de9a5a2e1bee2d4a
commit r12-5090-g94396a27bcfbdcb156586688de9a5a2e1bee2d4a
Author: Yannick Moy <moy@adacore.com>
Date: Tue Nov 2 15:43:42 2021 +0100
[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:
---
gcc/ada/Makefile.rtl | 1 +
.../libgnat/{a-nbnbin__ghost.adb => a-nbnbig.adb} | 11 ++++++++---
.../libgnat/{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(-)
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index fb3f6f60a41..282b25ce700 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 7d220869576..d04d2a4d019 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 3663dd7aea8..237bca19b57 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 fce8c7ad3e0..79a0074214d 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 dcced7e40e6..e1bcf531b71 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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-11-10 8:58 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-11-10 8:58 [gcc r12-5090] [Ada] Create explicit ghost mirror unit for big integers Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).