https://gcc.gnu.org/g:5772cf81657acb20550ca627bcbd7e7ade26ff26
commit r16-6604-g5772cf81657acb20550ca627bcbd7e7ade26ff26 Author: Claire Dross <[email protected]> Date: Tue Nov 25 17:40:31 2025 +0100 ada: Fix Ultimate_Overlaid_Entity to match the SPARK RM semantics 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. Diff: --- 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 0d9f20a714f0..ae98ad6c98f7 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 ad7c0e647f09..dfbe15b5d2a5 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 ab0f305425d7..146fd10202a5 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.
