public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-2034] [Ada] Reject overlays in Global/Depends/Initializes contracts
@ 2021-07-05 13:15 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-07-05 13:15 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:59748b7180590360d3608d30e707a27b0b2cb476
commit r12-2034-g59748b7180590360d3608d30e707a27b0b2cb476
Author: Piotr Trojanek <trojanek@adacore.com>
Date: Fri Apr 30 00:29:33 2021 +0200
[Ada] Reject overlays in Global/Depends/Initializes contracts
gcc/ada/
* sem_prag.adb (Analyze_Depends_In_Decl_Part): Reject overlays
in Depends and Refined_Depends contracts.
(Analyze_Global_In_Decl_Part): Likewise for Global and
Refined_Global.
(Analyze_Initializes_In_Decl_Part): Likewise for Initializes
(when appearing both as a single item and as a initialization
clause).
* sem_util.ads (Ultimate_Overlaid_Entity): New routine.
* sem_util.adb (Report_Unused_Body_States): Ignore overlays.
(Ultimate_Overlaid_Entity): New routine.
Diff:
---
gcc/ada/sem_prag.adb | 44 ++++++++++++++++++++++++++++++++++++++++++++
gcc/ada/sem_util.adb | 40 ++++++++++++++++++++++++++++++++++++++++
gcc/ada/sem_util.ads | 9 +++++++++
3 files changed, 93 insertions(+)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0efdceff5e7..41e887d8f39 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1139,6 +1139,17 @@ package body Sem_Prag is
(State_Id => Item_Id,
Ref => Item);
end if;
+
+ elsif Ekind (Item_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Item_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Depends",
+ Item, Item_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Item, Ultimate_Overlaid_Entity (Item_Id));
+ return;
end if;
-- When the item renames an entire object, replace the
@@ -2387,6 +2398,17 @@ package body Sem_Prag is
elsif Is_Formal_Object (Item_Id) then
null;
+ elsif Ekind (Item_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Item_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Global",
+ Item, Item_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Item, Ultimate_Overlaid_Entity (Item_Id));
+ return;
+
-- The only legal references are those to abstract states,
-- objects and various kinds of constants (SPARK RM 6.1.4(4)).
@@ -2984,6 +3006,16 @@ package body Sem_Prag is
if Item_Id = Any_Id then
null;
+ elsif Ekind (Item_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Item_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Initializes",
+ Item, Item_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Item, Ultimate_Overlaid_Entity (Item_Id));
+
-- The state or variable must be declared in the visible
-- declarations of the package (SPARK RM 7.1.5(7)).
@@ -3126,6 +3158,18 @@ package body Sem_Prag is
end if;
end if;
+ if Ekind (Input_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Input_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Initializes",
+ Input, Input_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Input, Ultimate_Overlaid_Entity (Input_Id));
+ return;
+ end if;
+
-- Detect a duplicate use of the same input item
-- (SPARK RM 7.1.5(5)).
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7ea809bf5a6..038c1ee686b 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5708,6 +5708,13 @@ package body Sem_Util is
if Ekind (State_Id) = E_Constant then
null;
+ -- Overlays do not contribute to package state
+
+ elsif Ekind (State_Id) = E_Variable
+ and then Present (Ultimate_Overlaid_Entity (State_Id))
+ then
+ null;
+
-- Generate an error message of the form:
-- body of package ... has unused hidden states
@@ -29312,6 +29319,39 @@ package body Sem_Util is
end if;
end Type_Without_Stream_Operation;
+ ------------------------------
+ -- Ultimate_Overlaid_Entity --
+ ------------------------------
+
+ function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id is
+ Address : Node_Id;
+ Alias : Entity_Id := E;
+ Offset : Boolean;
+
+ begin
+ -- Currently this routine is only called for stand-alone objects that
+ -- have been analysed, since the analysis of the Address aspect is often
+ -- delayed.
+
+ pragma Assert (Ekind (E) in E_Constant | E_Variable);
+
+ loop
+ Address := Address_Clause (Alias);
+ if Present (Address) then
+ Find_Overlaid_Entity (Address, Alias, Offset);
+ if Present (Alias) then
+ null;
+ else
+ return Empty;
+ end if;
+ elsif Alias = E then
+ return Empty;
+ else
+ return Alias;
+ end if;
+ end loop;
+ end Ultimate_Overlaid_Entity;
+
---------------------
-- Ultimate_Prefix --
---------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index a49272e080f..7cacae2f907 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -3275,6 +3275,15 @@ package Sem_Util is
-- prevents the construction of a composite stream operation. If Op is
-- specified we check only for the given stream operation.
+ function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id;
+ -- If entity E is overlaying some other entity via an Address clause (which
+ -- possibly overlays yet another entity via its own Address clause), then
+ -- return the ultimate overlaid entity. If entity E is not overlaying any
+ -- other entity (or the overlaid entity cannot be determined statically),
+ -- then return Empty.
+ --
+ -- Subsidiary to the analysis of object overlays in SPARK.
+
function Ultimate_Prefix (N : Node_Id) return Node_Id;
-- Obtain the "outermost" prefix of arbitrary node N. Return N if no such
-- prefix exists.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-07-05 13:15 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-07-05 13:15 [gcc r12-2034] [Ada] Reject overlays in Global/Depends/Initializes contracts 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).