From: Claire Dross <[email protected]>
The Ultimate_Overlaid_Entity function should return the root of the
last precisely supported address clause as per the definition in the
SPARK RM.
gcc/ada/ChangeLog:
* sem_util.ads (Overlaid_Entity): Return the root of the address
clause of an object if it is precisely supported in SPARK.
* sem_util.adb (Ultimate_Overlaid_Entity): Use Overlaid_Entity to
match the SPARK RM semantics.
* sem_prag.adb (Analyze_Global_Item): Only check for overlays on
variables.
(Analyze_Initialization_Item): Likewise.
(Analyze_Input_Item): Likewise.
Tested on x86_64-pc-linux-gnu (before the recent bootstrap breakage), committed
on master.
---
gcc/ada/sem_prag.adb | 8 ++--
gcc/ada/sem_util.adb | 97 +++++++++++++++++++++++++++++++++++---------
gcc/ada/sem_util.ads | 18 +++++---
3 files changed, 94 insertions(+), 29 deletions(-)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0d9f20a714f..ae98ad6c98f 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1361,7 +1361,7 @@ package body Sem_Prag is
Ref => Item);
end if;
- elsif Ekind (Item_Id) in E_Constant | E_Variable
+ elsif Ekind (Item_Id) = E_Variable
and then Present (Ultimate_Overlaid_Entity (Item_Id))
then
SPARK_Msg_NE
@@ -3286,7 +3286,7 @@ package body Sem_Prag is
elsif Is_Formal_Object (Item_Id) then
null;
- elsif Ekind (Item_Id) in E_Constant | E_Variable
+ elsif Ekind (Item_Id) = E_Variable
and then Present (Ultimate_Overlaid_Entity (Item_Id))
then
SPARK_Msg_NE
@@ -3910,7 +3910,7 @@ package body Sem_Prag is
if Item_Id = Any_Id then
null;
- elsif Ekind (Item_Id) in E_Constant | E_Variable
+ elsif Ekind (Item_Id) = E_Variable
and then Present (Ultimate_Overlaid_Entity (Item_Id))
then
SPARK_Msg_NE
@@ -4062,7 +4062,7 @@ package body Sem_Prag is
end if;
end if;
- if Ekind (Input_Id) in E_Constant | E_Variable
+ if Ekind (Input_Id) = E_Variable
and then Present (Ultimate_Overlaid_Entity (Input_Id))
then
SPARK_Msg_NE
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index ad7c0e647f0..dfbe15b5d2a 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -26639,6 +26639,71 @@ package body Sem_Util is
Write_Eol;
end Output_Name;
+ ---------------------
+ -- Overlaid_Entity --
+ ---------------------
+
+ function Overlaid_Entity (E : Entity_Id) return Entity_Id is
+ Address : Node_Id;
+
+ begin
+ if Ekind (E) in E_Constant | E_Variable then
+ Address := Address_Clause (E);
+ else
+ return Empty;
+ end if;
+
+ if Present (Address) then
+ declare
+ Expr : Node_Id := Expression (Address);
+
+ begin
+ -- Only support precisely address clauses of the form P'Address
+
+ if Nkind (Expr) = N_Attribute_Reference
+ and then Attribute_Name (Expr) = Name_Address
+ then
+ Expr := Prefix (Expr);
+
+ else
+ return Empty;
+ end if;
+
+ loop
+
+ -- Precisely supported addresses refer to part of objects
+
+ if Is_Entity_Name (Expr) then
+ if Is_Object (Entity (Expr)) then
+ return Entity (Expr);
+ else
+ return Empty;
+ end if;
+
+ elsif Nkind (Expr) in N_Selected_Component
+ | N_Indexed_Component
+ | N_Explicit_Dereference
+ then
+ Expr := Prefix (Expr);
+
+ -- Taking the address of a slice is only well-defined if the
+ -- components are aliased.
+
+ elsif Nkind (Expr) = N_Slice
+ and then Has_Aliased_Components (Etype (Etype (Expr)))
+ then
+ Expr := Prefix (Expr);
+
+ else
+ return Empty;
+ end if;
+ end loop;
+ end;
+ else
+ return Empty;
+ end if;
+ end Overlaid_Entity;
+
------------------
-- Param_Entity --
------------------
@@ -29648,32 +29713,24 @@ package body Sem_Util is
------------------------------
function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id is
- Address : Node_Id;
- Alias : Entity_Id := E;
- Offset : Boolean;
- Ovrl_Typ : Entity_Id;
+ Alias : Entity_Id := E;
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);
+ -- Currently this routine is only called for objects that have been
+ -- analysed, since the analysis of the Address aspect is often delayed.
loop
- Address := Address_Clause (Alias);
- if Present (Address) then
- Find_Overlaid_Entity (Address, Alias, Ovrl_Typ, Offset);
- if Present (Alias) then
- null;
- else
+ declare
+ Address_Root : constant Entity_Id := Overlaid_Entity (Alias);
+ begin
+ if Present (Address_Root) then
+ Alias := Address_Root;
+ elsif Alias = E then
return Empty;
+ else
+ return Alias;
end if;
- elsif Alias = E then
- return Empty;
- else
- return Alias;
- end if;
+ end;
end loop;
end Ultimate_Overlaid_Entity;
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index ab0f305425d..146fd10202a 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -3431,12 +3431,20 @@ 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 Overlaid_Entity (E : Entity_Id) return Entity_Id;
+ -- This function implements the definition of precisely supported address
+ -- clause in SPARK. If E has an address clause of the form P'Address, where
+ -- P is a part of an object, return the root object of P. Otherwise, return
+ -- Empty.
+ --
+ -- Subsidiary to the analysis of object overlays in SPARK.
+
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.
+ -- If entity E is overlaying some other entity via a precisely supported
+ -- 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.
--
2.51.0
